rewrite < H5.
rewrite < sym_times.
apply plus_to_minus.
-apply eq_plus_to_le ? ? ? H3.
apply H3.
apply le_times_r.
apply lt_to_le.
rewrite < H3.
rewrite < sym_times.
apply plus_to_minus.
-apply eq_plus_to_le ? ? ? H5.
apply H5.
apply le_times_r.
apply lt_to_le.
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.