-theorem eq_mod_O_to_lt_O_div: \forall n,m:nat. O < m \to O < n\to mod n m = O \to O < div n m.
-intros 4.apply lt_O_n_elim m H.intros.
-apply lt_times_to_lt_r m1.
+theorem eq_mod_O_to_lt_O_div: \forall n,m:nat. O < m \to O < n\to n \mod m = O \to O < n / m.
+intros 4.apply (lt_O_n_elim m H).intros.
+apply (lt_times_to_lt_r m1).