+theorem mod_SO: \forall n:nat. mod n (S O) = O.
+intro.
+apply sym_eq.
+apply le_n_O_to_eq.
+apply le_S_S_to_le.
+apply lt_mod_m_m.
+apply le_n.
+qed.
+
+theorem div_SO: \forall n:nat. div n (S O) = n.
+intro.
+rewrite > (div_mod ? (S O)) in \vdash (? ? ? %)
+ [rewrite > mod_SO.
+ rewrite < plus_n_O.
+ apply times_n_SO
+ |apply le_n
+ ]
+qed.
+
+theorem or_div_mod: \forall n,q. O < q \to
+((S (n \mod q)=q) \land S n = (S (div n q)) * q \lor
+((S (n \mod q)<q) \land S n= (div n q) * q + S (n\mod q))).
+intros.
+elim (le_to_or_lt_eq ? ? (lt_mod_m_m n q H))
+ [right.split
+ [assumption
+ |rewrite < plus_n_Sm.
+ apply eq_f.
+ apply div_mod.
+ assumption
+ ]
+ |left.split
+ [assumption
+ |simplify.
+ rewrite > sym_plus.
+ rewrite < H1 in ⊢ (? ? ? (? ? %)).
+ rewrite < plus_n_Sm.
+ apply eq_f.
+ apply div_mod.
+ assumption
+ ]
+ ]
+qed.
+