From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 3 Oct 2005 08:13:33 +0000 (+0000)
Subject: Several changes. Proof of Fermat's little theorem completed.
X-Git-Tag: V_0_7_2_3~264
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fcc4e47ab6406a9a666471e017b81cf364195866;p=helm.git

Several changes. Proof of Fermat's little theorem completed.
---

diff --git a/helm/matita/library/nat/div_and_mod.ma b/helm/matita/library/nat/div_and_mod.ma
index 26e3dcc82..f79891b48 100644
--- a/helm/matita/library/nat/div_and_mod.ma
+++ b/helm/matita/library/nat/div_and_mod.ma
@@ -243,6 +243,14 @@ intro.elim n.simplify.reflexivity.
 simplify.reflexivity.
 qed.
 
+theorem lt_to_eq_mod:\forall n,m:nat. n < m \to n \mod m = n.
+intros.
+apply div_mod_spec_to_eq2 n m (n/m) (n \mod m) O n.
+apply div_mod_spec_div_mod.
+apply le_to_lt_to_lt O n m.apply le_O_n.assumption.
+constructor 1.
+assumption.reflexivity.
+qed.
 
 (* injectivity *)
 theorem injective_times_r: \forall n:nat.injective nat nat (\lambda m:nat.(S n)*m).
diff --git a/helm/matita/library/nat/fermat_little_theorem.ma b/helm/matita/library/nat/fermat_little_theorem.ma
index 5d04a7c81..b8ccac291 100644
--- a/helm/matita/library/nat/fermat_little_theorem.ma
+++ b/helm/matita/library/nat/fermat_little_theorem.ma
@@ -17,6 +17,101 @@ set "baseuri" "cic:/matita/nat/fermat_little_theorem".
 include "nat/exp.ma".
 include "nat/gcd.ma".
 include "nat/permutation.ma".
+include "nat/congruence.ma".
+
+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.
+apply lt_mod_m_m.
+simplify.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.
+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.
+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.
+rewrite > lt_to_eq_mod.
+simplify.apply le_S_S.assumption.
+simplify.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 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.
+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.
+(* i = n, j < n *)
+elim Hcut1.
+apply False_ind.
+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.
+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.
+(* 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.
+qed.
+
+(*
+theorem eq_fact_pi: \forall n,m:nat. n < m \to n! = pi n (S_mod m).
+intro.elim n.
+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).
+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.
+unfold prime in H.elim H.
+assumption.apply divides_to_le.simplify.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.
+assumption.apply H1.
+apply trans_lt ? (S n1).simplify. apply le_n.
+assumption.assumption.
+apply divides_times_to_divides.
+assumption.assumption.
+qed.
 
 theorem permut_mod: \forall p,a:nat. prime p \to
 \lnot divides p a\to permut (\lambda n.(mod (a*n) p)) (pred p).
@@ -89,10 +184,67 @@ apply trans_lt ? (S O).simplify.apply le_n.assumption.
 apply H4.
 qed.
 
-(*
-theorem bad : \forall p,a:nat. prime p \to \lnot divides p a \to
-mod (exp a (pred p)) p = (S O). 
+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 map_iter p (\lambda x.x) times (S O) = 
-map_iter p (\lambda n.(mod (a*n) p)) times (S O).
-*)
\ No newline at end of file
+cut O < a.
+cut O < p.
+cut O < pred p.
+apply divides_to_congruent.
+assumption.
+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)!.
+elim Hcut3.
+assumption.
+apply False_ind.
+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 < times_n_SO.
+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).
+assumption.
+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.
+apply permut_to_eq_map_iter_i.
+apply assoc_times.
+apply sym_times.
+rewrite < plus_n_Sm.rewrite < plus_n_O.
+rewrite < S_pred.
+apply permut_mod.assumption.
+assumption.assumption.
+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.
+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.
+elim Hcut.assumption.
+apply False_ind.apply H1.
+rewrite < H2.
+apply witness ? ? O.apply times_n_O.
+apply le_to_or_lt_eq.
+apply le_O_n.
+qed.
+
diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma
index 8302f7ce5..0c8780f7e 100644
--- a/helm/matita/library/nat/minus.ma
+++ b/helm/matita/library/nat/minus.ma
@@ -68,6 +68,18 @@ intros.simplify.reflexivity.
 intros.simplify.apply H.apply le_S_S_to_le.assumption.
 qed.
 
+theorem minus_plus_m_m: \forall n,m:nat.n = (n+m)-m.
+intros 2.
+generalize in match n.
+elim m.
+rewrite < minus_n_O.apply plus_n_O.
+elim n2.simplify.
+apply minus_n_n.
+rewrite < plus_n_Sm.
+change with S n3 = (S n3 + n1)-n1.
+apply H.
+qed.
+
 theorem plus_minus_m_m: \forall n,m:nat.
 m \leq n \to n = (n-m)+m.
 intros 2.
diff --git a/helm/matita/library/nat/permutation.ma b/helm/matita/library/nat/permutation.ma
index 3ea405245..5d99f657b 100644
--- a/helm/matita/library/nat/permutation.ma
+++ b/helm/matita/library/nat/permutation.ma
@@ -384,7 +384,7 @@ let rec invert_permut n f m \def
      |(S p) \Rightarrow invert_permut p f m]].
 
 theorem invert_permut_f: \forall f:nat \to nat. \forall n,m:nat.
-m \le n \to (\forall p:nat. f m = f p \to m = p) \to invert_permut n f (f m) = m.
+m \le n \to injn f n\to invert_permut n f (f m) = m.
 intros 4.
 elim H.
 apply nat_case1 m.
@@ -394,143 +394,250 @@ intros.simplify.
 rewrite > eqb_n_n (f (S m1)).simplify.reflexivity.
 simplify.
 rewrite > not_eq_to_eqb_false (f m) (f (S n1)).
-simplify.apply H2.assumption.
+simplify.apply H2.
+apply injn_Sn_n. assumption.
 simplify.intro.absurd m = S n1.
-apply H3.assumption.simplify.intro.
+apply H3.apply le_S.assumption.apply le_n.assumption.
+simplify.intro.
 apply not_le_Sn_n n1.rewrite < H5.assumption.
 qed.
 
+theorem injective_invert_permut: \forall f:nat \to nat. \forall n:nat.
+permut f n \to injn (invert_permut n f) n.
+intros.
+unfold injn.intros.
+cut bijn f n.
+unfold bijn in Hcut.
+generalize in match Hcut i H1.intro.
+generalize in match Hcut j H2.intro.
+elim H4.elim H6.
+elim H5.elim H9.
+rewrite < H8.
+rewrite < H11.
+apply eq_f.
+rewrite < invert_permut_f f n a.
+rewrite < invert_permut_f f n a1.
+rewrite > H8.
+rewrite > H11.
+assumption.assumption.
+unfold permut in H.elim H. assumption.
+assumption.
+unfold permut in H.elim H. assumption.
+apply permut_to_bijn.assumption.
+qed.
+
+theorem permut_invert_permut: \forall f:nat \to nat. \forall n:nat.
+permut f n \to permut (invert_permut n f) n.
+intros.unfold permut.split.
+intros.simplify.elim n.
+simplify.elim eqb i (f O).simplify.apply le_n.simplify.apply le_n.
+simplify.elim eqb i (f (S n1)).simplify.apply le_n.
+simplify.apply le_S. assumption.
+apply injective_invert_permut.assumption.
+qed.
+
+theorem f_invert_permut: \forall f:nat \to nat. \forall n,m:nat.
+m \le n \to permut f n\to f (invert_permut n f m) = m.
+intros.
+apply injective_invert_permut f n H1.
+unfold permut in H1.elim H1.
+apply H2.
+cut permut (invert_permut n f) n.unfold permut in Hcut.
+elim Hcut.apply H4.assumption.
+apply permut_invert_permut.assumption.assumption.
+(* uffa: lo ha espanso troppo *)
+change with invert_permut n f (f (invert_permut n f m)) = invert_permut n f m.
+apply invert_permut_f.
+cut permut (invert_permut n f) n.unfold permut in Hcut.
+elim Hcut.apply H2.assumption.
+apply permut_invert_permut.assumption.
+unfold permut in H1.elim H1.assumption.
+qed.
+
+theorem permut_n_to_eq_n: \forall h:nat \to nat.\forall n:nat.
+permut h n \to (\forall m:nat. m < n \to h m = m) \to h n = n.
+intros.unfold permut in H.elim H.
+cut invert_permut n h n < n \lor invert_permut n h n = n.
+elim Hcut.
+rewrite < f_invert_permut h n n in \vdash (? ? ? %).
+apply eq_f.
+rewrite < f_invert_permut h n n in \vdash (? ? % ?).
+apply H1.assumption.apply le_n.assumption.apply le_n.assumption.
+rewrite < H4 in \vdash (? ? % ?).
+apply f_invert_permut h.apply le_n.assumption.
+apply le_to_or_lt_eq.
+cut permut (invert_permut n h) n.
+unfold permut in Hcut.elim Hcut.
+apply H4.apply le_n.
+apply permut_invert_permut.assumption.
+qed.
+
+theorem permut_n_to_le: \forall h:nat \to nat.\forall k,n:nat.
+k \le n \to permut h n \to (\forall m:nat. m < k \to h m = m) \to 
+\forall j. k \le j \to j \le n \to k \le h j.
+intros.unfold permut in H1.elim H1.
+cut h j < k \lor \not(h j < k).
+elim Hcut.absurd k \le j.assumption.
+apply lt_to_not_le.
+cut h j = j.rewrite < Hcut1.assumption.
+apply H6.apply H5.assumption.assumption.
+apply H2.assumption.
+apply not_lt_to_le.assumption.
+apply decidable_lt (h j) k.
+qed.
+
 (* applications *)
 
-let rec map_iter n (g:nat \to nat) f (a:nat) \def
-  match n with
-   [ O \Rightarrow a
-   | (S p) \Rightarrow f (g p) (map_iter p g f a)].
-   
-theorem eq_map_iter: \forall g1,g2:nat \to nat.
-\forall f:nat \to nat \to nat. \forall n,a:nat.
-(\forall m:nat. m \lt n \to g1 m = g2 m) \to 
-map_iter n g1 f a = map_iter n g2 f a.
-intros 5.elim n.simplify.reflexivity.
-simplify.apply eq_f2.apply H1.simplify.apply le_n.
-apply H.intros.apply H1.apply trans_lt ? n1.assumption.
-simplify.apply le_n.
+let rec map_iter_i k (g:nat \to nat) f (i:nat) \def
+  match k with
+   [ O \Rightarrow g i
+   | (S k) \Rightarrow f (g (S (k+i))) (map_iter_i k g f i)].
+
+theorem eq_map_iter_i: \forall g1,g2:nat \to nat.
+\forall f:nat \to nat \to nat. \forall n,i:nat.
+(\forall m:nat. i\le m \to m \le n+i \to g1 m = g2 m) \to 
+map_iter_i n g1 f i = map_iter_i n g2 f i.
+intros 5.elim n.simplify.apply H.apply le_n.
+apply le_n.simplify.apply eq_f2.apply H1.simplify.
+apply le_S.apply le_plus_n.simplify.apply le_n.
+apply H.intros.apply H1.assumption.simplify.apply le_S.assumption.
 qed.
 
 (* map_iter examples *)
-theorem eq_map_iter_sigma: \forall g:nat \to nat. \forall n:nat. 
-map_iter n g plus O = sigma n g.
+
+theorem eq_map_iter_i_sigma: \forall g:nat \to nat. \forall n,m:nat. 
+map_iter_i n g plus m = sigma n g m.
 intros.elim n.simplify.reflexivity.
 simplify.
 apply eq_f.assumption.
 qed.
 
-theorem eq_map_iter_pi: \forall g:nat \to nat. \forall n:nat. 
-map_iter n g times (S O) = pi n g.
+theorem eq_map_iter_i_pi: \forall g:nat \to nat. \forall n,m:nat. 
+map_iter_i n g times m = pi n g m.
 intros.elim n.simplify.reflexivity.
 simplify.
 apply eq_f.assumption.
 qed.
 
-theorem eq_map_iter_transpose_i_Si : \forall f:nat\to nat \to nat.associative nat f \to
-symmetric2 nat nat f \to \forall g:nat \to nat. \forall n,i,a:nat. i \lt n \to
-map_iter (S n) g f a = map_iter (S n) (\lambda m. g (transpose i (S i) m)) f a.
-intros 5.elim n.apply False_ind.apply not_le_Sn_O i H2.
-simplify in H3.
-cut i < n1 \lor i = n1.
-change with 
-f (g (S n1)) (map_iter (S n1) g f a) = 
-f (g (transpose i (S i) (S n1))) (map_iter (S n1) (\lambda m. g (transpose i (S i) m)) f a).
-elim Hcut.
-cut g (transpose i (S i) (S n1)) = g (S n1).
-rewrite > Hcut1.
-rewrite < H2 i a H4.reflexivity.
-unfold transpose.
-rewrite > not_eq_to_eqb_false (S n1) i.
-rewrite > not_eq_to_eqb_false (S n1) (S i).
+theorem eq_map_iter_i_fact: \forall n:nat. 
+map_iter_i n (\lambda m.m) times (S O) = (S n)!.
+intros.elim n.
 simplify.reflexivity.
-simplify.intro.
-apply lt_to_not_eq i n1 H4.
-apply injective_S i.apply sym_eq.assumption.
-simplify. intro.
-apply lt_to_not_eq i (S n1).
-apply trans_lt ? n1.assumption.simplify.apply le_n.
-apply sym_eq.assumption.
-(* interesting case *)
-rewrite > H4.
-change with f (g (S n1)) (f (g n1) (map_iter n1 g f a)) = 
-f (g (transpose n1 (S n1) (S n1)))
-(f (g (transpose n1 (S n1) n1)) 
-(map_iter n1 (\lambda m. g (transpose n1 (S n1) m)) f a)).
-cut (g (transpose n1 (S n1) (S n1))) = g n1.
-cut (g (transpose n1 (S n1) n1)) = g (S n1).
-cut map_iter n1 (\lambda m. g (transpose n1 (S n1) m)) f a = map_iter n1 g f a.
-rewrite > Hcut1.rewrite > Hcut2.rewrite > Hcut3.
+change with 
+((S n1)+(S O))*(map_iter_i n1 (\lambda m.m) times (S O)) = (S(S n1))*(S n1)!.
+rewrite < plus_n_Sm.rewrite < plus_n_O.
+apply eq_f.assumption.
+qed.
+
+theorem eq_map_iter_i_transpose_l : \forall f:nat\to nat \to nat.associative nat f \to
+symmetric2 nat nat f \to \forall g:nat \to nat. \forall n,k:nat. 
+map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose (k+n) (S k+n) m)) f n.
+intros.apply nat_case1 k.
+intros.simplify.
+change with
+f (g (S n)) (g n) = 
+f (g (transpose n (S n) (S n))) (g (transpose n (S n) n)).
+rewrite > transpose_i_j_i.
+rewrite > transpose_i_j_j.
+apply H1.
+intros.
+change with 
+f (g (S (S (m+n)))) (f (g (S (m+n))) (map_iter_i m g f n)) = 
+f (g (transpose (S m + n) (S (S m) + n) (S (S m)+n))) 
+(f (g (transpose (S m + n) (S (S m) + n) (S m+n))) 
+(map_iter_i m (\lambda m1. g (transpose (S m+n) (S (S m)+n) m1)) f n)).
+rewrite > transpose_i_j_i.
+rewrite > transpose_i_j_j.
+rewrite < H.
 rewrite < H.
-rewrite > H1 (g (S n1)).
-rewrite > H.reflexivity.
-apply eq_map_iter.
+rewrite < H1 (g (S m + n)).
+apply eq_f.
+apply eq_map_iter_i.
 intros.unfold transpose.
-rewrite > not_eq_to_eqb_false m n1.
-rewrite > not_eq_to_eqb_false m (S n1).
+rewrite > not_eq_to_eqb_false m1 (S m+n).
+rewrite > not_eq_to_eqb_false m1 (S (S m)+n).
+simplify.
+reflexivity.
+apply lt_to_not_eq m1 (S (S m)+n).
+simplify.apply le_S_S.apply le_S.assumption.
+apply lt_to_not_eq m1 (S m+n).
+simplify.apply le_S_S.assumption.
+qed.
+
+theorem eq_map_iter_i_transpose_i_Si : \forall f:nat\to nat \to nat.associative nat f \to
+symmetric2 nat nat f \to \forall g:nat \to nat. \forall n,k,i:nat. n \le i \to i \le k+n \to
+map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i (S i) m)) f n.
+intros 6.elim k.cut i=n.
+rewrite > Hcut.
+apply eq_map_iter_i_transpose_l f H H1 g n O.
+apply antisymmetric_le.assumption.assumption.
+cut i < S n1 + n \lor i = S n1 + n.
+elim Hcut.
+change with 
+f (g (S (S n1)+n)) (map_iter_i (S n1) g f n) = 
+f (g (transpose i (S i) (S (S n1)+n))) (map_iter_i (S n1) (\lambda m. g (transpose i (S i) m)) f n).
+apply eq_f2.unfold transpose.
+rewrite > not_eq_to_eqb_false (S (S n1)+n) i.
+rewrite > not_eq_to_eqb_false (S (S n1)+n) (S i).
 simplify.reflexivity.
-simplify. intro.apply lt_to_not_eq m (S n1).
-apply trans_lt ? n1.assumption.simplify. apply le_n.
+simplify.intro.
+apply lt_to_not_eq i (S n1+n).assumption.
+apply inj_S.apply sym_eq. assumption.
+simplify.intro.
+apply lt_to_not_eq i (S (S n1+n)).simplify.
+apply le_S_S.assumption.
+apply sym_eq. assumption.
+apply H2.assumption.apply le_S_S_to_le.
 assumption.
-simplify. intro.apply lt_to_not_eq m n1.
-assumption.assumption.
-unfold transpose.
-rewrite > eqb_n_n n1.simplify.reflexivity.
-unfold transpose.
-rewrite > not_eq_to_eqb_false.simplify.
-rewrite > eqb_n_n n1.simplify.reflexivity.
-simplify. intro.
-apply not_eq_n_Sn n1. apply sym_eq.assumption.
-apply le_to_or_lt_eq.
-apply le_S_S_to_le.assumption.
+rewrite > H5.
+apply eq_map_iter_i_transpose_l f H H1 g n (S n1).
+apply le_to_or_lt_eq.assumption.
 qed.
 
-theorem eq_map_iter_transpose: \forall f:nat\to nat \to nat.associative nat f \to
-symmetric2 nat nat f \to \forall n,a,k:nat. 
-\forall g:nat \to nat. \forall i:nat. S (k + i) \le n \to  
-map_iter (S n) g  f a = map_iter (S n) (\lambda m. g (transpose i (S(k + i)) m)) f a.
+theorem eq_map_iter_i_transpose: 
+\forall f:nat\to nat \to nat.
+associative nat f \to symmetric2 nat nat f \to \forall n,k,o:nat. 
+\forall g:nat \to nat. \forall i:nat. n \le i \to S (o + i) \le S k+n \to  
+map_iter_i (S k) g  f n = map_iter_i (S k) (\lambda m. g (transpose i (S(o + i)) m)) f n.
 intros 6.
-apply nat_elim1 k.
+apply nat_elim1 o.
 intro.
 apply nat_case m ?.
 intros.
-apply eq_map_iter_transpose_i_Si ? H H1.
-exact H3.
+apply eq_map_iter_i_transpose_i_Si ? H H1.
+exact H3.apply le_S_S_to_le.assumption.
 intros.
-apply trans_eq ? ? (map_iter (S n) (\lambda m. g (transpose i (S(m1 + i)) m)) f a).
+apply trans_eq ? ? (map_iter_i (S k) (\lambda m. g (transpose i (S(m1 + i)) m)) f n).
 apply H2.
-simplify. apply le_n.
+simplify. apply le_n.assumption.
 apply trans_le ? (S(S (m1+i))).
 apply le_S.apply le_n.assumption.
-apply trans_eq ? ? (map_iter (S n) (\lambda m. g 
-(transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) m))) f a).
+apply trans_eq ? ? (map_iter_i (S k) (\lambda m. g 
+(transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) m))) f n).
 apply H2 O ? ? (S(m1+i)).
 simplify.apply le_S_S.apply le_O_n.
-exact H3.
-apply trans_eq ? ? (map_iter (S n) (\lambda m. g 
+apply trans_le ? i.assumption.
+change with i \le (S m1)+i.apply le_plus_n.
+exact H4.
+apply trans_eq ? ? (map_iter_i (S k) (\lambda m. g 
 (transpose i (S(m1 + i)) 
 (transpose (S(m1 + i)) (S(S(m1 + i))) 
-(transpose i (S(m1 + i)) m)))) f a).
-apply H2 m1 ?.
-simplify. apply le_n.
+(transpose i (S(m1 + i)) m)))) f n).
+apply H2 m1.
+simplify. apply le_n.assumption.
 apply trans_le ? (S(S (m1+i))).
 apply le_S.apply le_n.assumption.
-apply eq_map_iter.
+apply eq_map_iter_i.
 intros.apply eq_f.
 apply sym_eq. apply eq_transpose.
 simplify. intro.
 apply not_le_Sn_n i.
-rewrite < H5 in \vdash (? ? %).
+rewrite < H7 in \vdash (? ? %).
 apply le_S_S.apply le_S.
 apply le_plus_n.
 simplify. intro.
 apply not_le_Sn_n i.
-rewrite > H5 in \vdash (? ? %).
+rewrite > H7 in \vdash (? ? %).
 apply le_S_S.
 apply le_plus_n.
 simplify. intro.
@@ -538,189 +645,98 @@ apply not_eq_n_Sn (S m1+i).
 apply sym_eq.assumption.
 qed.
 
-theorem eq_map_iter_transpose1: \forall f:nat\to nat \to nat.associative nat f \to
-symmetric2 nat nat f \to \forall n,a,i,j:nat. 
-\forall g:nat \to nat. i < j \to j \le n \to 
-map_iter (S n) g f a = map_iter (S n) (\lambda m. g (transpose i j m)) f a.
+theorem eq_map_iter_i_transpose1: \forall f:nat\to nat \to nat.associative nat f \to
+symmetric2 nat nat f \to \forall n,k,i,j:nat. 
+\forall g:nat \to nat. n \le i \to i < j \to j \le S k+n \to 
+map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i j m)) f n.
 intros.
-simplify in H2.
+simplify in H3.
 cut (S i) < j \lor (S i) = j.
 elim Hcut.
 cut j = S ((j - (S i)) + i).
 rewrite > Hcut1.
-apply eq_map_iter_transpose f H H1 n a (j - (S i)) g i.
+apply eq_map_iter_i_transpose f H H1 n k (j - (S i)) g i.
+assumption.
 rewrite < Hcut1.assumption.
 rewrite > plus_n_Sm.
 apply plus_minus_m_m.apply lt_to_le.assumption.
-rewrite < H4.
-apply eq_map_iter_transpose_i_Si f H H1 g.
+rewrite < H5.
+apply eq_map_iter_i_transpose_i_Si f H H1 g.
 simplify.
+assumption.apply le_S_S_to_le.
 apply trans_le ? j.assumption.assumption.
 apply le_to_or_lt_eq.assumption.
 qed.
 
-theorem eq_map_iter_transpose2: \forall f:nat\to nat \to nat.associative nat f \to
-symmetric2 nat nat f \to \forall n,a,i,j:nat. 
-\forall g:nat \to nat. i \le n \to j \le n \to 
-map_iter (S n) g f a = map_iter (S n) (\lambda m. g (transpose i j m)) f a.
+theorem eq_map_iter_i_transpose2: \forall f:nat\to nat \to nat.associative nat f \to
+symmetric2 nat nat f \to \forall n,k,i,j:nat. 
+\forall g:nat \to nat. n \le i \to i \le (S k+n) \to n \le j \to j \le (S k+n) \to 
+map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i j m)) f n.
 intros.
 apply nat_compare_elim i j.
-intro.apply eq_map_iter_transpose1 f H H1 n a  i j g H4 H3.
-intro.rewrite > H4.
-apply eq_map_iter.intros.
+intro.apply eq_map_iter_i_transpose1 f H H1 n k i j g H2 H6 H5.
+intro.rewrite > H6.
+apply eq_map_iter_i.intros.
 rewrite > transpose_i_i j.reflexivity.
 intro.
-apply trans_eq ? ? (map_iter (S n) (\lambda m:nat.g (transpose j i m)) f a).
-apply eq_map_iter_transpose1 f H H1 n a j i g H4 H2.
-apply eq_map_iter.
+apply trans_eq ? ? (map_iter_i (S k) (\lambda m:nat.g (transpose j i m)) f n).
+apply eq_map_iter_i_transpose1 f H H1 n k j i g H4 H6 H3.
+apply eq_map_iter_i.
 intros.apply eq_f.apply transpose_i_j_j_i.
 qed.
 
-theorem permut_to_eq_map_iter:\forall f:nat\to nat \to nat.associative nat f \to
-symmetric2 nat nat f \to \forall a,n:nat.\forall g,h:nat \to nat.
-permut h n \to 
-map_iter (S n) g f a = map_iter (S n) (\lambda m.g(h m)) f a.
-intros 5.elim n.
-simplify.rewrite > permut_O_to_eq_O h.reflexivity.assumption.
-apply trans_eq ? ? (map_iter (S(S n1)) (\lambda m.g ((transpose (h (S n1)) (S n1)) m)) f a).
-apply eq_map_iter_transpose2 f H H1 (S n1) a ? ? g.
+theorem permut_to_eq_map_iter_i:\forall f:nat\to nat \to nat.associative nat f \to
+symmetric2 nat nat f \to \forall k,n:nat.\forall g,h:nat \to nat.
+permut h (k+n) \to (\forall m:nat. m \lt n \to h m = m) \to
+map_iter_i k g f n = map_iter_i k (\lambda m.g(h m)) f n.
+intros 4.elim k.
+simplify.rewrite > permut_n_to_eq_n h.reflexivity.assumption.assumption.
+apply trans_eq ? ? (map_iter_i (S n) (\lambda m.g ((transpose (h (S n+n1)) (S n+n1)) m)) f n1).
 unfold permut in H3.
-elim H3.apply H4.apply le_n.apply le_n.
-apply trans_eq ? ? (map_iter (S(S n1)) (\lambda m.
-(g(transpose (h (S n1)) (S n1) 
-(transpose (h (S n1)) (S n1) (h m)))) )f a).
+elim H3.
+apply eq_map_iter_i_transpose2 f H H1 n1 n ? ? g.
+apply permut_n_to_le h n1 (S n+n1).
+apply le_plus_n.assumption.assumption.apply le_plus_n.apply le_n.
+apply H5.apply le_n.apply le_plus_n.apply le_n.
+apply trans_eq ? ? (map_iter_i (S n) (\lambda m.
+(g(transpose (h (S n+n1)) (S n+n1) 
+(transpose (h (S n+n1)) (S n+n1) (h m)))) )f n1).
 change with
-f (g (transpose (h (S n1)) (S n1) (S n1)))
-(map_iter (S n1) (\lambda m.
-g (transpose (h (S n1)) (S n1) m)) f a)
+f (g (transpose (h (S n+n1)) (S n+n1) (S n+n1)))
+(map_iter_i n (\lambda m.
+g (transpose (h (S n+n1)) (S n+n1) m)) f n1)
 =
 f 
-(g(transpose (h (S n1)) (S n1) 
-(transpose (h (S n1)) (S n1) (h (S n1)))))
-(map_iter (S n1) 
+(g(transpose (h (S n+n1)) (S n+n1) 
+(transpose (h (S n+n1)) (S n+n1) (h (S n+n1)))))
+(map_iter_i n 
 (\lambda m.
-(g(transpose (h (S n1)) (S n1) 
-(transpose (h (S n1)) (S n1) (h m))))) f a).
+(g(transpose (h (S n+n1)) (S n+n1) 
+(transpose (h (S n+n1)) (S n+n1) (h m))))) f n1).
 apply eq_f2.apply eq_f.
 rewrite > transpose_i_j_j.
 rewrite > transpose_i_j_i.
 rewrite > transpose_i_j_j.reflexivity.
-apply H2 (\lambda m.(g(transpose (h (S n1)) (S n1) m))).
+apply H2 n1 (\lambda m.(g(transpose (h (S n+n1)) (S n+n1) m))).
 apply permut_S_to_permut_transpose.
 assumption.
-apply eq_map_iter.intros.
-rewrite > transpose_transpose.reflexivity.
-qed.
-
-theorem eq_sigma_transpose_i_Si: \forall n,i:nat. \forall f:nat \to nat. i \lt n \to
-sigma (S n) f = sigma (S n) (\lambda m. f (transpose i (S i) m)).
-intro.elim n.apply False_ind.apply not_le_Sn_O i H.
-simplify in H1.
-cut i < n1 \lor i = n1.
-change with 
-(f (S n1))+(sigma (S n1) f) = 
-(f (transpose i (S i) (S n1)))+(sigma (S n1) (\lambda m. f (transpose i (S i) m))).
-elim Hcut.
-cut f (transpose i (S i) (S n1)) = f (S n1).
-rewrite > Hcut1.
-rewrite < H i f.reflexivity.
-assumption.unfold transpose.
-rewrite > not_eq_to_eqb_false (S n1) i.
-rewrite > not_eq_to_eqb_false (S n1) (S i).
-simplify.reflexivity.
+intros.
+unfold transpose.
+rewrite > not_eq_to_eqb_false (h m) (h (S n+n1)).
+rewrite > not_eq_to_eqb_false (h m) (S n+n1).
+simplify.apply H4.assumption.
+rewrite > H4.
+apply lt_to_not_eq.apply trans_lt ? n1.assumption.
+simplify.apply le_S_S.apply le_plus_n.assumption.
+unfold permut in H3.elim H3.
 simplify.intro.
-apply lt_to_not_eq i n1 H2.
-apply injective_S i.apply sym_eq.assumption.
-simplify. intro.
-apply lt_to_not_eq i (S n1).
-apply trans_lt ? n1.assumption.simplify.apply le_n.
-apply sym_eq.assumption.
-rewrite > H2.
-change with (f (S n1))+((f n1)+(sigma n1 f)) = 
-(f (transpose n1 (S n1) (S n1)))+
-((f (transpose n1 (S n1) n1))+
-(sigma n1 (\lambda m. f (transpose n1 (S n1) m)))).
-cut (f (transpose n1 (S n1) (S n1))) = f n1.
-cut (f (transpose n1 (S n1) n1)) = f (S n1).
-cut sigma n1 (\lambda m. f (transpose n1 (S n1) m)) = sigma n1 f.
-rewrite > Hcut1.rewrite > Hcut2.rewrite > Hcut3.
-rewrite < assoc_plus.rewrite > sym_plus (f (S n1)).
-rewrite > assoc_plus.reflexivity.
-apply eq_sigma.
-intros.unfold transpose.
-rewrite > not_eq_to_eqb_false m n1.
-rewrite > not_eq_to_eqb_false m (S n1).
-simplify.reflexivity.
-simplify. intro.apply lt_to_not_eq m (S n1).
-apply trans_lt ? n1.assumption.simplify. apply le_n.
+apply lt_to_not_eq m (S n+n1).apply trans_lt ? n1.assumption.
+simplify.apply le_S_S.apply le_plus_n.
+unfold injn in H7.
+apply H7 m (S n+n1).apply trans_le ? n1.
+apply lt_to_le.assumption.apply le_plus_n.apply le_n.
 assumption.
-simplify. intro.apply lt_to_not_eq m n1.
-assumption.assumption.
-unfold transpose.
-rewrite > eqb_n_n n1.simplify.reflexivity.
-unfold transpose.
-rewrite > not_eq_to_eqb_false.simplify.
-rewrite > eqb_n_n n1.simplify.reflexivity.
-simplify. intro.
-apply not_eq_n_Sn n1. apply sym_eq.assumption.
-apply le_to_or_lt_eq.
-apply le_S_S_to_le.assumption.
-qed.
-
-theorem eq_sigma_transpose: \forall n,k:nat. \forall f:nat \to nat. 
-\forall i. S (k + i) \le n \to
-sigma (S n) f = sigma (S n) (\lambda m. f (transpose i (S(k + i)) m)).
-intros 2.
-apply nat_elim1 k.
-intro.
-apply nat_case m ?.
-intros.
-apply eq_sigma_transpose_i_Si n i f.
-exact H1.
-intros.
-apply trans_eq ? ? (sigma (S n) (\lambda m. f (transpose i (S(m1 + i)) m))).
-apply H m1 ? f ?.
-simplify. apply le_n.
-apply trans_le ? (S(S (m1+i))).
-apply le_S.apply le_n.assumption.
-apply trans_eq ? ? (sigma (S n) (\lambda m. f 
-(transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) m)))).
-apply H O ? ? (S(m1+i)) ?.
-simplify.apply le_S_S.apply le_O_n.
-exact H1.
-apply trans_eq ? ? (sigma (S n) (\lambda m. f 
-(transpose i (S(m1 + i)) 
-(transpose (S(m1 + i)) (S(S(m1 + i))) 
-(transpose i (S(m1 + i)) m))))).
-apply H m1 ? ? i.
-simplify. apply le_n.
-apply trans_le ? (S(S (m1+i))).
-apply le_S.apply le_n.assumption.
-apply eq_sigma.
-intros.apply eq_f.
-apply sym_eq. apply eq_transpose.
-simplify. intro.
-apply not_le_Sn_n i.
-rewrite < H3 in \vdash (? ? %).
-apply le_S_S.apply le_S.
-apply le_plus_n.
-simplify. intro.
-apply not_le_Sn_n i.
-rewrite > H3 in \vdash (? ? %).
-apply le_S_S.
-apply le_plus_n.
-simplify. intro.
-apply not_eq_n_Sn (S m1+i).
-apply sym_eq.assumption.
+apply eq_map_iter_i.intros.
+rewrite > transpose_transpose.reflexivity.
 qed.
 
-(*
-theorem bad: \forall n:nat. \forall f:nat \to nat.
-permut f n \to sigma (S n) f = sigma (S n) (\lambda n.n). 
-intro.elim n.
-simplify.unfold permut in H.elim H O.
-rewrite < (le_n_O_to_eq (f O)).simplify. reflexivity.apply le_n.
-cut permut (\lambda n.transpose (f (S n1)) (S n1) (f n)) n1.
-apply trans_eq ? ? 
-(sigma (S(S n1)) (\lambda n.transpose (f (S n1)) (S n1) (f n))).
-*)
\ No newline at end of file
diff --git a/helm/matita/library/nat/primes.ma b/helm/matita/library/nat/primes.ma
index 1d0fed296..691356243 100644
--- a/helm/matita/library/nat/primes.ma
+++ b/helm/matita/library/nat/primes.ma
@@ -72,6 +72,10 @@ theorem divides_n_O: \forall n:nat. n \divides O.
 intro. apply witness n O O.apply times_n_O.
 qed.
 
+theorem divides_n_n: \forall n:nat. n \divides n.
+intro. apply witness n n (S O).apply times_n_SO.
+qed.
+
 theorem divides_SO_n: \forall n:nat. (S O) \divides n.
 intro. apply witness (S O) n n. simplify.apply plus_n_O.
 qed.
@@ -247,21 +251,23 @@ reflexivity.
 qed.
 
 (* divides and pi *)
-theorem divides_f_pi_f : \forall f:nat \to nat.\forall n,i:nat. 
-i < n \to f i \divides pi n f.
-intros 3.elim n.apply False_ind.apply not_le_Sn_O i H.
+theorem divides_f_pi_f : \forall f:nat \to nat.\forall n,m,i:nat. 
+m \le i \to i \le n+m \to f i \divides pi n f m.
+intros 5.elim n.simplify.
+cut i = m.rewrite < Hcut.apply divides_n_n.
+apply antisymmetric_le.assumption.assumption.
 simplify.
-apply le_n_Sm_elim (S i) n1 H1.
-intro.
-apply transitive_divides ? (pi n1 f).
-apply H.simplify.apply le_S_S_to_le. assumption.
-apply witness ? ? (f n1).apply sym_times.
-intro.cut i = n1.
-rewrite > Hcut.
-apply witness ? ? (pi n1 f).reflexivity.
-apply inj_S.assumption.
+cut i < S n1+m \lor i = S n1 + m.
+elim Hcut.
+apply transitive_divides ? (pi n1 f m).
+apply H1.apply le_S_S_to_le. assumption.
+apply witness ? ? (f (S n1+m)).apply sym_times.
+rewrite > H3.
+apply witness ? ? (pi n1 f m).reflexivity.
+apply le_to_or_lt_eq.assumption.
 qed.
 
+(*
 theorem mod_S_pi: \forall f:nat \to nat.\forall n,i:nat. 
 i < n \to (S O) < (f i) \to (S (pi n f)) \mod (f i) = (S O).
 intros.cut (pi n f) \mod (f i) = O.
@@ -271,6 +277,7 @@ rewrite > Hcut.assumption.
 apply divides_to_mod_O.apply trans_lt O (S O).apply le_n (S O).assumption.
 apply divides_f_pi_f.assumption.
 qed.
+*)
 
 (* divides and fact *)
 theorem divides_fact : \forall n,i:nat. 
diff --git a/helm/matita/library/nat/relevant_equations.ma b/helm/matita/library/nat/relevant_equations.ma
index fee1fd407..1c0f25f57 100644
--- a/helm/matita/library/nat/relevant_equations.ma
+++ b/helm/matita/library/nat/relevant_equations.ma
@@ -15,6 +15,7 @@
 set "baseuri" "cic:/matita/nat/relevant_equations.ma".
 
 include "nat/times.ma".
+include "nat/minus.ma".
 
 theorem times_plus_l: \forall n,m,p:nat. (n+m)*p = n*p + m*p.
 intros.
@@ -27,6 +28,17 @@ apply sym_times.
 apply sym_times.
 qed.
 
+theorem times_minus_l: \forall n,m,p:nat. (n-m)*p = n*p - m*p.
+intros.
+apply trans_eq ? ? (p*(n-m)).
+apply sym_times.
+apply trans_eq ? ? (p*n-p*m).
+apply distr_times_minus.
+apply eq_f2.
+apply sym_times.
+apply sym_times.
+qed.
+
 theorem times_plus_plus: \forall n,m,p,q:nat. (n + m)*(p + q) =
 n*p + n*q + m*p + m*q.
 intros.
diff --git a/helm/matita/library/nat/sigma_and_pi.ma b/helm/matita/library/nat/sigma_and_pi.ma
index 6bd6af38c..331df8fb3 100644
--- a/helm/matita/library/nat/sigma_and_pi.ma
+++ b/helm/matita/library/nat/sigma_and_pi.ma
@@ -16,42 +16,64 @@ set "baseuri" "cic:/matita/nat/sigma_and_pi".
 
 include "nat/factorial.ma".
 include "nat/lt_arith.ma".
+include "nat/exp.ma".
 
-let rec sigma n f \def
+let rec sigma n f m \def
   match n with 
-  [ O \Rightarrow O
-  | (S p) \Rightarrow (f p)+(sigma p f)].
+  [ O \Rightarrow (f m)
+  | (S p) \Rightarrow (f (S p+m))+(sigma p f m)].
 
-let rec pi n f \def
+let rec pi n f m \def
   match n with 
-  [ O \Rightarrow (S O)
-  | (S p) \Rightarrow (f p)*(pi p f)].
+  [ O \Rightarrow f m
+  | (S p) \Rightarrow (f (S p+m))*(pi p f m)].
   
 theorem eq_sigma: \forall f,g:nat \to nat.
-\forall n:nat. (\forall m:nat. m < n \to f m = g m) \to
-(sigma n f) = (sigma n g).
+\forall n,m:nat.
+(\forall i:nat. m \le i \to i \le m+n \to f i = g i) \to
+(sigma n f m) = (sigma n g m).
 intros 3.elim n.
-simplify.reflexivity.
+simplify.apply H.apply le_n.rewrite < plus_n_O.apply le_n.
 simplify.
-apply eq_f2.apply H1.simplify. apply le_n.
-apply H.intros.apply H1.
-apply trans_lt ? n1.assumption.simplify.apply le_n.
+apply eq_f2.apply H1.
+change with m \le (S n1)+m.apply le_plus_n.
+rewrite > sym_plus m.apply le_n.
+apply H.intros.apply H1.assumption.
+rewrite < plus_n_Sm.
+apply le_S.assumption.
 qed.
 
 theorem eq_pi: \forall f,g:nat \to nat.
-\forall n:nat. (\forall m:nat. m < n \to f m = g m) \to
-(pi n f) = (pi n g).
+\forall n,m:nat.
+(\forall i:nat. m \le i \to i \le m+n \to f i = g i) \to
+(pi n f m) = (pi n g m).
 intros 3.elim n.
-simplify.reflexivity.
+simplify.apply H.apply le_n.rewrite < plus_n_O.apply le_n.
 simplify.
-apply eq_f2.apply H1.simplify. apply le_n.
-apply H.intros.apply H1.
-apply trans_lt ? n1.assumption.simplify.apply le_n.
+apply eq_f2.apply H1.
+change with m \le (S n1)+m.apply le_plus_n.
+rewrite > sym_plus m.apply le_n.
+apply H.intros.apply H1.assumption.
+rewrite < plus_n_Sm.
+apply le_S.assumption.
 qed.
 
-theorem eq_fact_pi: \forall n. n! = pi n S.
+theorem eq_fact_pi: \forall n. (S n)! = pi n (\lambda m.m) (S O).
 intro.elim n.
 simplify.reflexivity.
-change with (S n1)*n1! = (S n1)*(pi n1 S).
+change with (S(S n1))*(S n1)! = ((S n1)+(S O))*(pi n1 (\lambda m.m) (S O)).
+rewrite < plus_n_Sm.rewrite < plus_n_O.
 apply eq_f.assumption.
-qed.
\ No newline at end of file
+qed.
+
+theorem exp_pi_l: \forall f:nat\to nat.\forall n,m,a:nat.
+(exp a (S n))*pi n f m= pi n (\lambda p.a*(f p)) m.
+intros.elim n.simplify.rewrite < times_n_SO.reflexivity.
+simplify.
+rewrite < H.
+rewrite > assoc_times. 
+rewrite > assoc_times in\vdash (? ?  ? %).
+apply eq_f.rewrite < assoc_times. 
+rewrite < assoc_times. 
+apply eq_f2.apply sym_times.reflexivity.
+qed.