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=b8ccac29140bb71de8656c920d89b4016907f210;hpb=fcc4e47ab6406a9a666471e017b81cf364195866;p=helm.git

diff --git a/helm/matita/library/nat/fermat_little_theorem.ma b/helm/matita/library/nat/fermat_little_theorem.ma
index b8ccac291..cc18a8bb9 100644
--- a/helm/matita/library/nat/fermat_little_theorem.ma
+++ b/helm/matita/library/nat/fermat_little_theorem.ma
@@ -23,62 +23,62 @@ theorem permut_S_mod: \forall n:nat. permut (S_mod (S n)) n.
 intro.unfold permut.split.intros.
 unfold S_mod.
 apply le_S_S_to_le.
-change with (S i) \mod (S n) < S n.
+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).
-rewrite < lt_to_eq_mod j (S n).
-cut i < n \lor i = n.
-cut j < n \lor j = n.
+rewrite < (lt_to_eq_mod i (S n)).
+rewrite < (lt_to_eq_mod j (S n)).
+cut (i < n \lor i = n).
+cut (j < n \lor j = n).
 elim Hcut.
 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.
 apply False_ind.
-apply not_eq_O_S (i \mod (S n)).
+apply (not_eq_O_S (i \mod (S n))).
 apply sym_eq.
-rewrite < mod_n_n (S n).
+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.
-apply not_eq_O_S (j \mod (S n)).
-rewrite < mod_n_n (S n).
+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.
 
 (*
@@ -88,26 +88,26 @@ simplify.reflexivity.
 change with (S n1)*n1!=(S_mod m n1)*(pi n1 (S_mod m)).
 unfold S_mod in \vdash (? ? ? (? % ?)). 
 rewrite > lt_to_eq_mod.
-apply eq_f.apply H.apply trans_lt ? (S n1).
+apply eq_f.apply H.apply (trans_lt ? (S n1)).
 simplify. apply le_n.assumption.assumption.
 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.
-apply lt_to_not_le (S O) p.
+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.
+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.
+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.
@@ -117,108 +117,108 @@ theorem permut_mod: \forall p,a:nat. prime p \to
 \lnot divides p a\to permut (\lambda n.(mod (a*n) p)) (pred p).
 unfold permut.intros.
 split.intros.apply le_S_S_to_le.
-apply trans_le ? p.
-change with mod (a*i) p < p.
+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.
+apply (nat_compare_elim i j).
 (* i < j *)
 intro.
-absurd j-i \lt p.
-simplify.
-rewrite > S_pred p.
+absurd (j-i \lt p).
+unfold lt.
+rewrite > (S_pred p).
 apply le_S_S.
 apply le_plus_to_minus.
-apply trans_le ? (pred p).assumption.
+apply (trans_le ? (pred p)).assumption.
 rewrite > sym_plus.
 apply le_plus_n.
 unfold prime in H.
 elim H.
-apply trans_lt ? (S O).simplify.apply le_n.assumption.
-apply le_to_not_lt p (j-i).
-apply divides_to_le.simplify.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption.
+apply (le_to_not_lt p (j-i)).
+apply divides_to_le.unfold lt.
 apply le_SO_minus.assumption.
-cut divides p a \lor divides p (j-i).
+cut (divides p a \lor divides p (j-i)).
 elim Hcut.apply False_ind.apply H1.assumption.assumption.
 apply divides_times_to_divides.assumption.
 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 *)
 intro. assumption.
 (* j < i *)
 intro.
-absurd i-j \lt p.
-simplify.
-rewrite > S_pred p.
+absurd (i-j \lt p).
+unfold lt.
+rewrite > (S_pred p).
 apply le_S_S.
 apply le_plus_to_minus.
-apply trans_le ? (pred p).assumption.
+apply (trans_le ? (pred p)).assumption.
 rewrite > sym_plus.
 apply le_plus_n.
 unfold prime in H.
 elim H.
-apply trans_lt ? (S O).simplify.apply le_n.assumption.
-apply le_to_not_lt p (i-j).
-apply divides_to_le.simplify.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption.
+apply (le_to_not_lt p (i-j)).
+apply divides_to_le.unfold lt.
 apply le_SO_minus.assumption.
-cut divides p a \lor divides p (i-j).
+cut (divides p a \lor divides p (i-j)).
 elim Hcut.apply False_ind.apply H1.assumption.assumption.
 apply divides_times_to_divides.assumption.
 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.
 
 theorem congruent_exp_pred_SO: \forall p,a:nat. prime p \to \lnot divides p a \to
 congruent (exp a (pred p)) (S O) p. 
 intros.
-cut O < a.
-cut O < p.
-cut O < pred p.
+cut (O < a).
+cut (O < p).
+cut (O < pred p).
 apply divides_to_congruent.
 assumption.
-change with O < exp a (pred p).
+change with (O < exp a (pred p)).
 apply lt_O_exp.assumption.
-cut divides p (exp a (pred p)-(S O)) \lor divides p (pred p)!.
+cut (divides p (exp a (pred p)-(S O)) \lor divides p (pred p)!).
 elim Hcut3.
 assumption.
 apply False_ind.
-apply prime_to_not_divides_fact p H (pred p).
-change with S (pred p) \le p.
+apply (prime_to_not_divides_fact p H (pred p)).
+change with (S (pred p) \le p).
 rewrite < S_pred.apply le_n.
 assumption.assumption.
 apply divides_times_to_divides. 
 assumption.
 rewrite > times_minus_l.
-rewrite > sym_times (S O).
+rewrite > (sym_times (S O)).
 rewrite < times_n_SO.
-rewrite > S_pred (pred p).
+rewrite > (S_pred (pred p)).
 rewrite > eq_fact_pi.
 (* in \vdash (? ? (? % ?)). *)
 rewrite > exp_pi_l.
 apply congruent_to_divides.
 assumption. 
-apply transitive_congruent p ? 
-(pi (pred (pred p)) (\lambda m. a*m \mod p) (S O)).
-apply congruent_pi (\lambda m. a*m).
+apply (transitive_congruent p ? 
+(pi (pred (pred p)) (\lambda m. a*m \mod p) (S O))).
+apply (congruent_pi (\lambda m. a*m)).
 assumption.
-cut pi (pred(pred p)) (\lambda m.m) (S O)
-= pi (pred(pred p)) (\lambda m.a*m \mod p) (S O).
+cut (pi (pred(pred p)) (\lambda m.m) (S O)
+= pi (pred(pred p)) (\lambda m.a*m \mod p) (S O)).
 rewrite > Hcut3.apply congruent_n_n.
 rewrite < eq_map_iter_i_pi.
 rewrite < eq_map_iter_i_pi.
@@ -229,21 +229,21 @@ rewrite < plus_n_Sm.rewrite < plus_n_O.
 rewrite < S_pred.
 apply permut_mod.assumption.
 assumption.assumption.
-intros.cut m=O.
+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.
+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.
-cut O < a \lor O = a.
+unfold prime in H.elim H.apply (trans_lt ? (S O)).
+unfold lt.apply le_n.assumption.
+cut (O < a \lor O = a).
 elim Hcut.assumption.
 apply False_ind.apply H1.
 rewrite < H2.
-apply witness ? ? O.apply times_n_O.
+apply (witness ? ? O).apply times_n_O.
 apply le_to_or_lt_eq.
 apply le_O_n.
 qed.