X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fdiv_and_mod.ma;h=e9831f82ad1ec5cc01decf9e920f9e80518c3f64;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=9995830a9061b1662447a6d8f99329b4f4e50430;hpb=fb94e5a71be508516514dfe50528ccfb3cd2da91;p=helm.git

diff --git a/helm/matita/library/nat/div_and_mod.ma b/helm/matita/library/nat/div_and_mod.ma
index 9995830a9..e9831f82a 100644
--- a/helm/matita/library/nat/div_and_mod.ma
+++ b/helm/matita/library/nat/div_and_mod.ma
@@ -70,7 +70,7 @@ qed.
 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.
 
@@ -108,7 +108,7 @@ definition div_mod_spec : nat \to nat \to nat \to nat \to Prop \def
 *)
 
 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.
@@ -188,7 +188,7 @@ 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.
 
@@ -198,7 +198,7 @@ intros.
 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.