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

diff --git a/helm/matita/library/nat/fermat_little_theorem.ma b/helm/matita/library/nat/fermat_little_theorem.ma
index bbd5e359a..cc18a8bb9 100644
--- a/helm/matita/library/nat/fermat_little_theorem.ma
+++ b/helm/matita/library/nat/fermat_little_theorem.ma
@@ -25,7 +25,7 @@ unfold S_mod.
 apply le_S_S_to_le.
 change with ((S i) \mod (S n) < S n).
 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 injn.intros.
 apply inj_S.
 rewrite < (lt_to_eq_mod i (S n)).
@@ -37,14 +37,14 @@ elim Hcut1.
 (* i < n, j< n *)
 rewrite < mod_S.
 rewrite < mod_S.
-apply H2.simplify.apply le_S_S.apply le_O_n.
+apply H2.unfold lt.apply le_S_S.apply le_O_n.
 rewrite > lt_to_eq_mod.
-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.apply le_O_n.
 rewrite > lt_to_eq_mod.
-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.
 (* i < n, j=n *)
 unfold S_mod in H2.
 simplify.
@@ -54,11 +54,11 @@ apply sym_eq.
 rewrite < (mod_n_n (S n)).
 rewrite < H4 in \vdash (? ? ? (? %?)).
 rewrite < mod_S.assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 rewrite > lt_to_eq_mod.
-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.apply le_O_n.
 (* i = n, j < n *)
 elim Hcut1.
 apply False_ind.
@@ -66,19 +66,19 @@ apply (not_eq_O_S (j \mod (S n))).
 rewrite < (mod_n_n (S n)).
 rewrite < H3 in \vdash (? ? (? %?) ?).
 rewrite < mod_S.assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 rewrite > lt_to_eq_mod.
-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.apply le_O_n.
 (* i = n, j= n*)
 rewrite > H3.
 rewrite > H4.
 reflexivity.
 apply le_to_or_lt_eq.assumption.
 apply le_to_or_lt_eq.assumption.
-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.
 qed.
 
 (*
@@ -95,19 +95,19 @@ qed.
 
 theorem prime_to_not_divides_fact: \forall p:nat. prime p \to \forall n:nat.
 n \lt p \to \not divides p n!.
-intros 3.elim n.simplify.intros.
+intros 3.elim n.unfold Not.intros.
 apply (lt_to_not_le (S O) p).
 unfold prime in H.elim H.
-assumption.apply divides_to_le.simplify.apply le_n.
+assumption.apply divides_to_le.unfold lt.apply le_n.
 assumption.
 change with (divides p ((S n1)*n1!) \to False).
 intro.
 cut (divides p (S n1) \lor divides p n1!).
 elim Hcut.apply (lt_to_not_le (S n1) p).
 assumption.
-apply divides_to_le.simplify.apply le_S_S.apply le_O_n.
+apply divides_to_le.unfold lt.apply le_S_S.apply le_O_n.
 assumption.apply H1.
-apply (trans_lt ? (S n1)).simplify. apply le_n.
+apply (trans_lt ? (S n1)).unfold lt. apply le_n.
 assumption.assumption.
 apply divides_times_to_divides.
 assumption.assumption.
@@ -120,19 +120,19 @@ split.intros.apply le_S_S_to_le.
 apply (trans_le ? p).
 change with (mod (a*i) p < p).
 apply lt_mod_m_m.
-simplify in H.elim H.
-simplify.apply (trans_le ? (S (S O))).
+unfold prime in H.elim H.
+unfold lt.apply (trans_le ? (S (S O))).
 apply le_n_Sn.assumption.
 rewrite < S_pred.apply le_n.
 unfold prime in H.
 elim H.
-apply (trans_lt ? (S O)).simplify.apply le_n.assumption.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption.
 unfold injn.intros.
 apply (nat_compare_elim i j).
 (* i < j *)
 intro.
 absurd (j-i \lt p).
-simplify.
+unfold lt.
 rewrite > (S_pred p).
 apply le_S_S.
 apply le_plus_to_minus.
@@ -141,9 +141,9 @@ rewrite > sym_plus.
 apply le_plus_n.
 unfold prime in H.
 elim H.
-apply (trans_lt ? (S O)).simplify.apply le_n.assumption.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption.
 apply (le_to_not_lt p (j-i)).
-apply divides_to_le.simplify.
+apply divides_to_le.unfold lt.
 apply le_SO_minus.assumption.
 cut (divides p a \lor divides p (j-i)).
 elim Hcut.apply False_ind.apply H1.assumption.assumption.
@@ -152,7 +152,7 @@ rewrite > distr_times_minus.
 apply eq_mod_to_divides.
 unfold prime in H.
 elim H.
-apply (trans_lt ? (S O)).simplify.apply le_n.assumption.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption.
 apply sym_eq.
 apply H4.
 (* i = j *)
@@ -160,7 +160,7 @@ intro. assumption.
 (* j < i *)
 intro.
 absurd (i-j \lt p).
-simplify.
+unfold lt.
 rewrite > (S_pred p).
 apply le_S_S.
 apply le_plus_to_minus.
@@ -169,9 +169,9 @@ rewrite > sym_plus.
 apply le_plus_n.
 unfold prime in H.
 elim H.
-apply (trans_lt ? (S O)).simplify.apply le_n.assumption.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption.
 apply (le_to_not_lt p (i-j)).
-apply divides_to_le.simplify.
+apply divides_to_le.unfold lt.
 apply le_SO_minus.assumption.
 cut (divides p a \lor divides p (i-j)).
 elim Hcut.apply False_ind.apply H1.assumption.assumption.
@@ -180,7 +180,7 @@ rewrite > distr_times_minus.
 apply eq_mod_to_divides.
 unfold prime in H.
 elim H.
-apply (trans_lt ? (S O)).simplify.apply le_n.assumption.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption.
 apply H4.
 qed.
 
@@ -238,7 +238,7 @@ change with ((S O) \le pred p).
 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)).
-simplify.apply le_n.assumption.
+unfold lt.apply le_n.assumption.
 cut (O < a \lor O = a).
 elim Hcut.assumption.
 apply False_ind.apply H1.