64 "change" here and there in the library are now simplify/unfold as they

[helm.git] / helm / software / matita / library / nat / fermat_little_theorem.ma

diff --git a/helm/software/matita/library/nat/fermat_little_theorem.ma b/helm/software/matita/library/nat/fermat_little_theorem.ma
index cc18a8bb9e4249005d96e772d7e41f4d01409720..e5c2ffd5dc26f632540733ab8b7a3b1afc1962ec 100644 (file)
--- a/helm/software/matita/library/nat/fermat_little_theorem.ma
+++ b/helm/software/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)).