theorem lt_mod_m_m: \forall n,m. O < m \to (n \mod m) < m.
intros 2.elim m.apply False_ind.
apply (not_le_Sn_O O H).
-simplify.apply le_S_S.apply le_mod_aux_m_m.
+simplify.unfold lt.apply le_S_S.apply le_mod_aux_m_m.
apply le_n.
qed.
*)
theorem div_mod_spec_to_not_eq_O: \forall n,m,q,r.(div_mod_spec n m q r) \to m \neq O.
-intros 4.simplify.intros.elim H.absurd (le (S r) O).
+intros 4.unfold Not.intros.elim H.absurd (le (S r) O).
rewrite < H1.assumption.
exact (not_le_Sn_O r).
qed.
theorem div_mod_spec_times : \forall n,m:nat.div_mod_spec ((S n)*m) (S n) m O.
intros.constructor 1.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
rewrite < plus_n_O.rewrite < sym_times.reflexivity.
qed.
apply (div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O).
goal 15. (* ?11 is closed with the following tactics *)
apply div_mod_spec_div_mod.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
apply div_mod_spec_times.
qed.