+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.