X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fnat%2Ffermat_little_theorem.ma;h=e5c2ffd5dc26f632540733ab8b7a3b1afc1962ec;hb=2fa59f0450a2f1fe871a09fd9841ddc1bfd67080;hp=cc18a8bb9e4249005d96e772d7e41f4d01409720;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/matita/library/nat/fermat_little_theorem.ma b/matita/library/nat/fermat_little_theorem.ma
index cc18a8bb9..e5c2ffd5d 100644
--- a/matita/library/nat/fermat_little_theorem.ma
+++ b/matita/library/nat/fermat_little_theorem.ma
@@ -199,7 +199,7 @@ elim Hcut3.
 assumption.
 apply False_ind.
 apply (prime_to_not_divides_fact p H (pred p)).
-change with (S (pred p) \le p).
+unfold lt.
 rewrite < S_pred.apply le_n.
 assumption.assumption.
 apply divides_times_to_divides. 
@@ -233,8 +233,7 @@ intros.cut (m=O).
 rewrite > Hcut3.rewrite < times_n_O.
 apply mod_O_n.apply sym_eq.apply le_n_O_to_eq.
 apply le_S_S_to_le.assumption.
-assumption.
-change with ((S O) \le pred p).
+assumption.unfold lt.
 apply le_S_S_to_le.rewrite < S_pred.
 unfold prime in H.elim H.assumption.assumption.
 unfold prime in H.elim H.apply (trans_lt ? (S O)).