X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fcount.ma;h=20913fa6041c103527cfd73e7a5c7708b15924de;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=60bdbadc4c228ebc5019eea85d783fd70e00757d;hpb=cca04138889cd0dbafb669a5c3fd8abe424d699e;p=helm.git

diff --git a/helm/matita/library/nat/count.ma b/helm/matita/library/nat/count.ma
index 60bdbadc4..20913fa60 100644
--- a/helm/matita/library/nat/count.ma
+++ b/helm/matita/library/nat/count.ma
@@ -78,7 +78,7 @@ rewrite < plus_n_O.
 rewrite < H.
 rewrite > (S_pred ((S n1)*(S m))).
 apply sigma_plus1.
-simplify.apply le_S_S.apply le_O_n.
+simplify.unfold lt.apply le_S_S.apply le_O_n.
 qed.
 
 theorem eq_sigma_sigma1 : \forall n,m:nat.\forall f:nat \to nat.
@@ -138,15 +138,15 @@ rewrite > (div_mod_spec_to_eq2 (i1*(S n) + i) (S n) ((i1*(S n) + i)/(S n))
                                         ((i1*(S n) + i) \mod (S n)) i1 i).
 rewrite > H3.
 apply bool_to_nat_andb.
-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
 apply div_mod_spec_div_mod.
-simplify.apply le_S_S.apply le_O_n.
-constructor 1.simplify.apply le_S_S.assumption.
+unfold lt.apply le_S_S.apply le_O_n.
+constructor 1.unfold lt.apply le_S_S.assumption.
 reflexivity.
 apply div_mod_spec_div_mod.
-simplify.apply le_S_S.apply le_O_n.
-constructor 1.simplify.apply le_S_S.assumption.
+unfold lt.apply le_S_S.apply le_O_n.
+constructor 1.unfold lt.apply le_S_S.assumption.
 reflexivity.
 apply (trans_eq ? ? 
 (sigma n (\lambda n.((bool_to_nat (f1 n)) *
@@ -170,13 +170,13 @@ rewrite < S_pred in \vdash (? ? %).
 change with ((g (i/(S n)) (i \mod (S n))) \lt (S n)*(S m)).
 apply H.
 apply lt_mod_m_m.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
 apply (lt_times_to_lt_l n).
 apply (le_to_lt_to_lt ? i).
 rewrite > (div_mod i (S n)) in \vdash (? ? %).
 rewrite > sym_plus.
 apply le_plus_n.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
 unfold lt.
 rewrite > S_pred in \vdash (? ? %).
 apply le_S_S.
@@ -184,12 +184,12 @@ rewrite > plus_n_O in \vdash (? ? %).
 rewrite > sym_times. assumption.
 rewrite > (times_n_O O).
 apply lt_times.
-simplify. apply le_S_S.apply le_O_n.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
 rewrite > (times_n_O O).
 apply lt_times.
-simplify. apply le_S_S.apply le_O_n.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
 rewrite < plus_n_O.
 unfold injn.
 intros.
@@ -206,40 +206,40 @@ rewrite < (H2 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3) in \vdash (? ? (? % ?) ?).
 rewrite < (H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5).
 rewrite < (H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5) in \vdash (? ? ? (? % ?)).
 rewrite > H6.reflexivity.
-simplify. apply le_S_S.apply le_O_n.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
 apply (lt_times_to_lt_l n).
 apply (le_to_lt_to_lt ? j).
 rewrite > (div_mod j (S n)) in \vdash (? ? %).
 rewrite > sym_plus.
 apply le_plus_n.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
 rewrite < sym_times. assumption.
 apply lt_mod_m_m.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
 apply (lt_times_to_lt_l n).
 apply (le_to_lt_to_lt ? i).
 rewrite > (div_mod i (S n)) in \vdash (? ? %).
 rewrite > sym_plus.
 apply le_plus_n.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
 rewrite < sym_times. assumption.
 apply lt_mod_m_m.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
 unfold lt.
 rewrite > S_pred in \vdash (? ? %).
 apply le_S_S.assumption.
 rewrite > (times_n_O O).
 apply lt_times.
-simplify. apply le_S_S.apply le_O_n.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
 unfold lt.
 rewrite > S_pred in \vdash (? ? %).
 apply le_S_S.assumption.
 rewrite > (times_n_O O).
 apply lt_times.
-simplify. apply le_S_S.apply le_O_n.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
 intros.
 apply False_ind.
 apply (not_le_Sn_O m1 H4).