+theorem div_n_n: \forall n:nat. O < n \to n / n = S O.
+intros.
+apply (div_mod_spec_to_eq n n (n / n) (n \mod n) (S O) O).
+apply div_mod_spec_div_mod.assumption.
+constructor 1.assumption.
+rewrite < plus_n_O.simplify.rewrite < plus_n_O.reflexivity.
+qed.
+
+theorem eq_div_O: \forall n,m. n < m \to n / m = O.
+intros.
+apply (div_mod_spec_to_eq n m (n/m) (n \mod m) O n).
+apply div_mod_spec_div_mod.
+apply (le_to_lt_to_lt O n m).
+apply le_O_n.assumption.
+constructor 1.assumption.reflexivity.
+qed.
+
+theorem mod_n_n: \forall n:nat. O < n \to n \mod n = O.
+intros.
+apply (div_mod_spec_to_eq2 n n (n / n) (n \mod n) (S O) O).
+apply div_mod_spec_div_mod.assumption.
+constructor 1.assumption.
+rewrite < plus_n_O.simplify.rewrite < plus_n_O.reflexivity.
+qed.
+
+theorem mod_S: \forall n,m:nat. O < m \to S (n \mod m) < m \to
+((S n) \mod m) = S (n \mod m).
+intros.
+apply (div_mod_spec_to_eq2 (S n) m ((S n) / m) ((S n) \mod m) (n / m) (S (n \mod m))).
+apply div_mod_spec_div_mod.assumption.
+constructor 1.assumption.rewrite < plus_n_Sm.
+apply eq_f.
+apply div_mod.
+assumption.
+qed.
+
+theorem mod_O_n: \forall n:nat.O \mod n = O.
+intro.elim n.simplify.reflexivity.
+simplify.reflexivity.
+qed.
+
+theorem lt_to_eq_mod:\forall n,m:nat. n < m \to n \mod m = n.
+intros.
+apply (div_mod_spec_to_eq2 n m (n/m) (n \mod m) O n).
+apply div_mod_spec_div_mod.
+apply (le_to_lt_to_lt O n m).apply le_O_n.assumption.
+constructor 1.
+assumption.reflexivity.
+qed.
+
+(* injectivity *)