X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Ftotient.ma;h=24c3920ed82571324c2977a7be798b492fbf43e7;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=ff425772cd276d31b239c15bb35d5f5e6345ef50;hpb=cca04138889cd0dbafb669a5c3fd8abe424d699e;p=helm.git

diff --git a/helm/matita/library/nat/totient.ma b/helm/matita/library/nat/totient.ma
index ff425772c..24c3920ed 100644
--- a/helm/matita/library/nat/totient.ma
+++ b/helm/matita/library/nat/totient.ma
@@ -68,35 +68,35 @@ rewrite < H4.
 rewrite > sym_gcd.
 rewrite > gcd_mod.
 apply (gcd_times_SO_to_gcd_SO ? ? (S m2)).
-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.
 assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 rewrite < H5.
 rewrite > sym_gcd.
 rewrite > gcd_mod.
 apply (gcd_times_SO_to_gcd_SO ? ? (S m)).
-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 > sym_times.
 assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 intro.
 apply eqb_elim.
 intro.apply eqb_elim.
 intro.apply False_ind.
 apply H6.
 apply eq_gcd_times_SO.
-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 < gcd_mod.
 rewrite > H4.
 rewrite > sym_gcd.assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 rewrite < gcd_mod.
 rewrite > H5.
 rewrite > sym_gcd.assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 intro.reflexivity.
 intro.reflexivity.
 qed.
\ No newline at end of file