From f14ac9cceaaa7f1905f0dbc4548d24c4abe940e3 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Sat, 5 Jan 2013 16:22:16 +0000
Subject: [PATCH] Ported permutation.ma and fermat_little_theorem.ma

---
 matita/matita/lib/arithmetics/congruence.ma   | 119 +++----
 .../lib/arithmetics/fermat_little_theorem.ma  | 176 +++++++++
 matita/matita/lib/arithmetics/permutation.ma  | 333 ++++++++++++++++++
 matita/matita/lib/arithmetics/sigma_pi.ma     |  11 +
 4 files changed, 574 insertions(+), 65 deletions(-)
 create mode 100644 matita/matita/lib/arithmetics/fermat_little_theorem.ma
 create mode 100644 matita/matita/lib/arithmetics/permutation.ma

diff --git a/matita/matita/lib/arithmetics/congruence.ma b/matita/matita/lib/arithmetics/congruence.ma
index d9792b5eb..075a1c6c3 100644
--- a/matita/matita/lib/arithmetics/congruence.ma
+++ b/matita/matita/lib/arithmetics/congruence.ma
@@ -11,25 +11,17 @@
 
 include "arithmetics/primes.ma".
 
-(* successor mod n *)
-definition S_mod: nat → nat → nat ≝
-λn,m:nat. (S m) \mod n.
+definition S_mod ≝ λn,m:nat. S m \mod n.
 
-definition congruent: nat → nat → nat → Prop ≝
-λn,m,p:nat. mod n p = mod m p.
+definition congruent ≝ λn,m,p:nat. mod n p = mod m p.
 
 interpretation "congruent" 'congruent n m p = (congruent n m p).
 
-notation "hvbox(n break ≅_{p} m)"
-  non associative with precedence 45
-  for @{ 'congruent $n $m $p }.
-  
-theorem congruent_n_n: ∀n,p:nat.n ≅_{p} n .
+theorem congruent_n_n: ∀n,p:nat.congruent n n p.
 // qed.
 
-theorem transitive_congruent: 
-  ∀p.transitive nat (λn,m.congruent n m p).
-/2/ qed.
+theorem transitive_congruent: ∀p. transitive ? (λn,m. congruent n m p).
+// qed.
 
 theorem le_to_mod: ∀n,m:nat. n < m → n = n \mod m.
 #n #m #ltnm @(div_mod_spec_to_eq2 n m O n (n/m) (n \mod m))
@@ -37,82 +29,79 @@ theorem le_to_mod: ∀n,m:nat. n < m → n = n \mod m.
 qed.
 
 theorem mod_mod : ∀n,p:nat. O<p → n \mod p = (n \mod p) \mod p.
-#n #p #posp >(div_mod (n \mod p) p) in ⊢ (? ? % ?); 
+#n #p #posp >(div_mod (n \mod p) p) in ⊢ (??%?);
 >(eq_div_O ? p) // @lt_mod_m_m //
 qed.
 
 theorem mod_times_mod : ∀n,m,p:nat. O<p → O<m → 
   n \mod p = (n \mod (m*p)) \mod p.
-#n #m #p #posp #posm
-@(div_mod_spec_to_eq2 n p (n/p) (n \mod p) 
-(n/(m*p)*m + (n \mod (m*p)/p))) 
+#n #m #p #posp #posm 
+@(div_mod_spec_to_eq2 n p (n/p) (n \mod p) (n/(m*p)*m + (n \mod (m*p)/p)))
   [@div_mod_spec_div_mod //
-  |% [@lt_mod_m_m //] >distributive_times_plus_r
-   >associative_plus <div_mod >associative_times <div_mod //
+  |% [@lt_mod_m_m //]
+   >distributive_times_plus_r >associative_plus <div_mod //
   ]
 qed.
 
-theorem congruent_n_mod_n : ∀n,p:nat. O < p →
- n ≅_{p} (n \mod p).
-/2/ qed.
+theorem congruent_n_mod_n: ∀n,p. 0 < p → 
+  congruent n (n \mod p) p.
+#n #p #posp @mod_mod //
+qed.
 
-theorem congruent_n_mod_times : ∀n,m,p:nat. O < p → O < m → 
-  n ≅_{p} (n \mod (m*p)).
-/2/ qed.
+theorem congruent_n_mod_times: ∀n,m,p. 0 < p → 0 < m → 
+  congruent n (n \mod (m*p)) p.
+#n #p #posp @mod_times_mod 
+qed.
 
-theorem eq_times_plus_to_congruent: ∀n,m,p,r:nat. O< p → 
-  n = r*p+m → n ≅_{p} m .
-#n #m #p #r #posp #eqn
+theorem eq_times_plus_to_congruent: ∀n,m,p,r:nat. 0 < p → 
+  n = r*p+m → congruent n m p.
+#n #m #p #r #posp #Hn
 @(div_mod_spec_to_eq2 n p (div n p) (mod n p) (r +(div m p)) (mod m p))
   [@div_mod_spec_div_mod //
-  |% [@lt_mod_m_m //] >distributive_times_plus_r
-   >associative_plus <div_mod //
+  |% [@lt_mod_m_m //]
+   >commutative_times >distributive_times_plus >commutative_times 
+   >(commutative_times p) >associative_plus //
   ]
 qed.
 
-theorem divides_to_congruent: ∀n,m,p:nat. O < p → m ≤ n → 
-  p ∣(n - m) → n ≅_{p} m .
-#n #m #p #posp #lemn * #l #eqpl 
-@(eq_times_plus_to_congruent … l posp) /2/
+theorem divides_to_congruent: ∀n,m,p:nat. 0 < p → m ≤ n → 
+  divides p (n - m) → congruent n m p.
+#n #m #p #posp #lemn * #q #Hdiv @(eq_times_plus_to_congruent n m p q) //
+>commutative_plus @minus_to_plus //
 qed.
 
-theorem congruent_to_divides: ∀n,m,p:nat.O < p → 
-  n ≅_{p} m → p ∣ (n - m).
-#n #m #p #posp #congnm @(quotient ? ? ((n / p)-(m / p)))
+theorem congruent_to_divides: ∀n,m,p:nat.
+  0 < p → congruent n m p → divides p (n - m).
+#n #m #p #posp #Hcong %{((n / p)-(m / p))}
 >commutative_times >(div_mod n p) in ⊢ (??%?);
->(div_mod m p) in ⊢ (??%?); <(commutative_plus (m \mod p))
-<congnm <(minus_plus ? (n \mod p)) <minus_plus_m_m //
+>(div_mod m p) in ⊢ (??%?); //
 qed.
 
-theorem mod_times: ∀n,m,p:nat. O < p → 
-  n*m ≅_{p} (n \mod p)*(m \mod p).
-#n #m #p #posp @(eq_times_plus_to_congruent ?? p 
+theorem mod_times: ∀n,m,p. 0 < p → 
+  mod (n*m) p = mod ((mod n p)*(mod m p)) p.
+#n #m #p #posp 
+@(eq_times_plus_to_congruent ? ? p 
   ((n / p)*p*(m / p) + (n / p)*(m \mod p) + (n \mod p)*(m / p))) //
-@(trans_eq ?? (((n/p)*p+(n \mod p))*((m/p)*p+(m \mod p))))
-  [@eq_f2 //
-  |@(trans_eq ? ? (((n/p)*p)*((m/p)*p) + (n/p)*p*(m \mod p) +
-    (n \mod p)*((m / p)*p) + (n \mod p)*(m \mod p))) //
-   >distributive_times_plus >distributive_times_plus_r 
-   >distributive_times_plus_r <associative_plus @eq_f2 //
+@(trans_eq ? ? (((n/p)*p+(n \mod p))*((m/p)*p+(m \mod p)))) //
+@(trans_eq ? ? (((n/p)*p)*((m/p)*p) + (n/p)*p*(m \mod p) +
+  (n \mod p)*((m / p)*p) + (n \mod p)*(m \mod p)))
+  [cut (∀a,b,c,d.(a+b)*(c+d) = a*c +a*d + b*c + b*d) 
+    [#a #b #c #d >(distributive_times_plus_r (c+d) a b) 
+     >(distributive_times_plus a c d)
+     >(distributive_times_plus b c d) //] #Hcut 
+   @Hcut
+  |@eq_f2
+    [<associative_times >(associative_times (n/p) p (m \mod p))
+     >(commutative_times p (m \mod p)) <(associative_times (n/p) (m \mod p) p)
+     >distributive_times_plus_r // 
+    |%
+    ]
   ]
 qed.
 
-theorem congruent_times: ∀n,m,n1,m1,p. O < p → 
-  n ≅_{p} n1 → m ≅_{p} m1 → n*m ≅_{p} n1*m1 .
-#n #m #n1 #m1 #p #posp #congn #congm
-@(transitive_congruent … (mod_times n m p posp))
->congn >congm @sym_eq @mod_times //
+theorem congruent_times: ∀n,m,n1,m1,p. O < p → congruent n n1 p → 
+  congruent m m1 p → congruent (n*m) (n1*m1) p.
+#n #m #n1 #m1 #p #posp #Hcongn #Hcongm whd
+>(mod_times n m p posp) >Hcongn >Hcongm @sym_eq @mod_times //
 qed.
 
-(*
-theorem congruent_pi: \forall f:nat \to nat. \forall n,m,p:nat.O < p \to
-congruent (pi n f m) (pi n (\lambda m. mod (f m) p) m) p.
-intros.
-elim n. simplify.
-apply congruent_n_mod_n.assumption.
-simplify.
-apply congruent_times.
-assumption.
-apply congruent_n_mod_n.assumption.
-assumption.
-qed. *)
diff --git a/matita/matita/lib/arithmetics/fermat_little_theorem.ma b/matita/matita/lib/arithmetics/fermat_little_theorem.ma
new file mode 100644
index 000000000..503eea682
--- /dev/null
+++ b/matita/matita/lib/arithmetics/fermat_little_theorem.ma
@@ -0,0 +1,176 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department of the University of Bologna, Italy.                     
+    ||I||                                                                 
+    ||T||  
+    ||A||  This file is distributed under the terms of the 
+    \   /  GNU General Public License Version 2        
+     \ /      
+      V_______________________________________________________________ *)
+
+include "arithmetics/exp.ma".
+include "arithmetics/gcd.ma".
+include "arithmetics/permutation.ma".
+include "arithmetics/congruence.ma".
+include "arithmetics/sigma_pi.ma".
+
+theorem permut_S_mod: ∀n:nat. permut (S_mod (S n)) n.
+#n %
+  [#i #lein @le_S_S_to_le @lt_mod_m_m //
+  |#i #j #lein #lejn #Heq @injective_S
+   <(lt_to_eq_mod i (S n)) [2: @le_S_S @lein]
+   <(lt_to_eq_mod j (S n)) [2: @le_S_S @lejn]
+   cases (le_to_or_lt_eq … lein) #Hi
+   cases (le_to_or_lt_eq … lejn) #Hj
+    [(* i < n, j< n *)
+     <mod_S 
+      [<mod_S 
+        [@Heq |@le_S_S >lt_to_eq_mod // @le_S // |//]
+      |@le_S_S >lt_to_eq_mod // @le_S // 
+      |//
+      ]
+    |(* i < n, j=n *)
+     @False_ind @(absurd ?? (not_eq_O_S (i \mod (S n))))
+     @sym_eq <(mod_n_n (S n)) [2://]
+     <Hj in ⊢ (???(?%?)); <mod_S
+      [@Heq |>lt_to_eq_mod [@le_S_S @Hi |@le_S_S @lt_to_le @Hi]|//]
+    |(* i = n, j < n *)
+     @False_ind @(absurd ?? (not_eq_O_S (j \mod (S n))))
+     <(mod_n_n (S n)) [2://]
+     <Hi in ⊢ (??(?%?)?); <mod_S
+      [@Heq |>lt_to_eq_mod [@le_S_S @Hj |@le_S_S @lt_to_le @Hj]|//]
+    |(* i = n, j= n*) 
+     >Hi >Hj %
+    ]
+  ]
+qed.
+
+theorem prime_to_not_divides_fact: ∀p.prime p → ∀n.n < p → p ∤ n!.
+#p #primep #n elim n 
+  [normalize #_ % #divp @(absurd (p ≤1)) 
+    [@divides_to_le // |@lt_to_not_le @prime_to_lt_SO //]
+  |#n1 #Hind #ltn1 whd in match (fact ?); % #Hdiv
+   cases (divides_times_to_divides … Hdiv)
+    [-Hdiv #Hdiv @(absurd … Hdiv) @Hind @lt_to_le //
+    |-Hdiv #Hdiv @(absurd … (p ≤ S n1))
+      [@divides_to_le // |@lt_to_not_le //]
+    |@primep
+    ]
+  ]
+qed.
+
+theorem permut_mod: ∀p,a:nat. prime p →
+  p ∤ a → permut (λn.(mod (a*n) p)) (pred p).
+#p #a #primep #ndiv % 
+  [#i #lei @le_S_S_to_le @(transitive_le ? p)
+    [@lt_mod_m_m @prime_to_lt_O //
+    |>S_pred [//| @prime_to_lt_O //]
+    ]
+  |#i #j #lei #lej #H cases (decidable_lt i j)
+    [(* i < j *) #ltij 
+     @False_ind @(absurd (j-i < p))
+      [<(S_pred p) [2:@prime_to_lt_O //] 
+       @le_S_S @le_plus_to_minus @(transitive_le … lej) //
+      |@le_to_not_lt @divides_to_le [@lt_plus_to_minus_r //] 
+       cut (p ∣ a ∨ p ∣ (j-i))
+        [2:* [#Hdiv @False_ind /2/ | //]]
+       @divides_times_to_divides // >distributive_times_minus
+       @eq_mod_to_divides // @prime_to_lt_O //
+      ]
+    |#Hij cases (le_to_or_lt_eq … (not_lt_to_le … Hij)) -Hij #Hij
+      [(* j < i *)
+       @False_ind @(absurd (i-j < p))
+        [<(S_pred p) [2:@prime_to_lt_O //] 
+         @le_S_S @le_plus_to_minus @(transitive_le … lei) //
+        |@le_to_not_lt @divides_to_le [@lt_plus_to_minus_r //] 
+         cut (p ∣ a ∨ p ∣ (i-j))
+          [2:* [#Hdiv @False_ind /2/ | //]]
+         @divides_times_to_divides // >distributive_times_minus
+         @eq_mod_to_divides // @prime_to_lt_O //
+        ]
+      |(* i = j *) //
+      ]
+    ]
+  ]
+qed.
+
+theorem eq_fact_pi_p:∀n.
+  fact n = ∏_{i ∈ [1,S n[ } i.
+#n elim n // #n1 #Hind whd in ⊢ (??%?); >commutative_times >bigop_Strue 
+  [cut (S n1 -1 = n1) [normalize //] #Hcut  
+   <plus_n_Sm <plus_n_O @eq_f <Hcut in ⊢ (???%); // | % ]
+qed.
+
+theorem congruent_pi: ∀f,n,p.O < p →
+  congruent (∏_{i < n}(f i)) (∏_{i < n} (mod (f i) p)) p.
+#f #n elim n // #n1 #Hind #p #posp >bigop_Strue //
+@congruent_times // [@congruent_n_mod_n // |@Hind //]
+qed. 
+
+theorem congruent_exp_pred_SO: ∀p,a:nat. prime p → ¬ divides p a →
+congruent (exp a (pred p)) (S O) p.
+#p #a #primep #ndiv 
+cut (0 < a) 
+  [lapply ndiv cases a // * #div0 @False_ind @div0 @(quotient ? 0 0) //] #posa 
+cut (O < p) [@prime_to_lt_O //] #posp
+cut (O < pred p) [@le_S_S_to_le >S_pred [@prime_to_lt_SO //| @posp] ] #pospred
+@(divides_to_congruent … posp) 
+  [@lt_O_exp //
+  |cut (divides p (exp a (pred p)-1) ∨ divides p (pred p)!)
+    [@divides_times_to_divides // >commutative_times
+     >distributive_times_minus <times_n_1
+     >eq_fact_pi_p >commutative_times 
+     cut (pred p = S (pred p) -1) [//] #Hpred >Hpred in match (exp a ?);
+     >exp_pi_bc @congruent_to_divides //
+     @(transitive_congruent p ? (∏_{i ∈ [1,S(pred p)[ }(a*i \mod p)))
+      [@(congruent_pi (λm.a*(m +1))) //
+      |cut (∏_{i ∈ [1,S(pred p)[ } i =  ∏_{i ∈ [1,S(pred p)[ } (a*i\mod p)) 
+        [2: #Heq <Heq @congruent_n_n]
+       >(bigop_I_gen 1 (S (pred p)) … 1 timesA) //
+       >(bigop_I_gen 1 (S (pred p)) … 1 timesA) //
+       @sym_eq @(bigop_iso … timesAC) 
+       lapply (permut_mod … primep ndiv) #Hpermut
+       %{(λi.a*i \mod p)} %{(invert_permut (pred p) (λi.a*i \mod p))} %
+        [%
+          [#i #lti #_ % 
+          |#i #lti #posi % 
+            [% 
+              [>(S_pred … posp) @lt_mod_m_m //
+              |>le_to_leb_true // 
+               cases (le_to_or_lt_eq … (le_O_n (a*i \mod p))) [//]
+               #H @False_ind @(absurd ? (mod_O_to_divides …(sym_eq  … H))) //
+               @(not_to_not … ndiv) #Hdiv cases(divides_times_to_divides … Hdiv)
+               // #divpi @False_ind @(absurd ? lti) @le_to_not_lt 
+               >(S_pred … posp) @divides_to_le // @leb_true_to_le 
+               @(andb_true_l … posi)
+              ]
+            |@invert_permut_f [@le_S_S_to_le //|cases Hpermut // ]
+            ]
+          ]
+        |lapply (permut_invert_permut … Hpermut) *
+         #le_invert_permut #inj_inv_permut
+         #i #lti #posi % 
+          [% 
+            [@le_S_S @le_invert_permut @le_S_S_to_le // 
+            |>le_to_leb_true //
+             cases (le_to_or_lt_eq … 
+               (le_O_n (invert_permut (pred p) (λi.a*i \mod p) i))) [//]
+             #H @False_ind
+             cut (a*0 \mod p = 0) [<times_n_O //] #H0 
+             cut (a*0 \mod p = a*(invert_permut (pred p) (λi.a*i \mod p) i) \mod p)
+               [@(eq_f ?? (λi.a*i \mod p)) //] 
+             >H0 >(f_invert_permut (λi.a*i \mod p) … Hpermut) [2:@le_S_S_to_le //]
+             #eq0i <eq0i in posi; normalize #H destruct (H)
+            ]
+          |@f_invert_permut [@le_S_S_to_le //| @Hpermut ]
+          ]
+        ]
+      ]
+    |* // #Hdiv @False_ind
+     @(absurd ? Hdiv (prime_to_not_divides_fact p primep (pred p) ?))
+     @le_S_S_to_le >S_pred //
+    ]
+  ]
+qed.
+
diff --git a/matita/matita/lib/arithmetics/permutation.ma b/matita/matita/lib/arithmetics/permutation.ma
new file mode 100644
index 000000000..2233c52fa
--- /dev/null
+++ b/matita/matita/lib/arithmetics/permutation.ma
@@ -0,0 +1,333 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department of the University of Bologna, Italy.                     
+    ||I||                                                                 
+    ||T||  
+    ||A||  This file is distributed under the terms of the 
+    \   /  GNU General Public License Version 2        
+     \ /      
+      V_______________________________________________________________ *)
+
+include "arithmetics/nat.ma".
+
+definition injn: (nat → nat) → nat → Prop ≝ λf,n.∀i,j:nat. 
+  i ≤ n → j ≤ n → f i = f j → i = j.
+
+theorem injn_Sn_n: ∀f,n. injn f (S n) → injn f n.
+#f #n #H #i #j #lei #lej #eqf @H [@le_S // |@le_S //|//] 
+qed.
+
+theorem injective_to_injn: ∀f,n. injective nat nat f → injn f n.
+#f #n #Hinj #i #j #_ #_ #eqf @Hinj // 
+qed.
+
+definition permut : (nat → nat) → nat → Prop 
+≝ λf,m.(∀i.i ≤ m → f i ≤ m )∧ injn f m.
+
+theorem permut_O_to_eq_O: ∀h.permut h O → h O = O.
+#h * #H1 #_ @sym_eq @le_n_O_to_eq @H1 //
+qed.
+
+theorem permut_S_to_permut: ∀f,m.
+  permut f (S m) → f (S m) = (S m) → permut f m.
+#f #m * #H1 #H2 #Hf %
+  [#i #leim cases(le_to_or_lt_eq … (H1 … (le_S … leim)))
+    [#H @le_S_S_to_le @H
+    |#H @False_ind @(absurd ? leim) @lt_to_not_le
+     lapply Hf <H in ⊢ (???%→?); -H #H <(H2 … H) // @le_S //
+    ]
+  |#i #j #lei #lej #eqf @H2 [@le_S //|@le_S // |//]
+  ]
+qed.
+
+(* transpositions *)
+
+definition transpose : nat → nat → nat → nat ≝ λi,j,n:nat. 
+  if eqb n i then j else if eqb n j then i else n.
+
+(*
+notation < "(❲i↹j❳) term 72 n" with precedence 71 
+for @{ 'transposition $i $j $n}.
+
+notation "(❲i \atop j❳) term 72 n" with precedence 71 
+for @{ 'transposition $i $j $n}.
+
+notation > "(❲\frac term 90 i term 90 j❳)n" with precedence 71 
+for @{ 'transposition $i $j $n}.
+*)
+
+interpretation "natural transposition" 'transposition i j n = (transpose i j n).
+
+lemma transpose_i_j_i: ∀i,j. transpose i j i = j.
+#i #j normalize >(eqb_n_n i) // 
+qed.
+
+lemma transpose_i_j_j: ∀i,j. transpose i j j = i.
+#i #j normalize cases(true_or_false (eqb j i)) #Hc 
+  [>Hc normalize >(eqb_true_to_eq … Hc) //  
+  |>Hc >(eqb_n_n j) //
+  ]
+qed.
+
+theorem transpose_i_i:  ∀i,n:nat. (transpose  i i n) = n.
+#i #n normalize cases (true_or_false (eqb n i)) #Hc >Hc
+  [normalize >(eqb_true_to_eq … Hc) // |// ]
+qed.
+
+theorem transpose_i_j_j_i: ∀i,j,n:nat.
+transpose i j n = transpose j i n.
+#i #j #n normalize cases (true_or_false (eqb n i)) #Hni >Hni
+cases (true_or_false (eqb n j)) #Hnj >Hnj normalize //
+<(eqb_true_to_eq … Hni) <(eqb_true_to_eq … Hnj) //
+qed.
+
+theorem transpose_transpose: ∀i,j,n:nat.
+  (transpose i j (transpose i j n)) = n.
+#i #j #n normalize cases (true_or_false (eqb n i)) #Hni >Hni normalize
+  [cases (true_or_false (eqb j i)) #Hji >Hji normalize
+    [>(eqb_true_to_eq … Hni) @(eqb_true_to_eq … Hji) 
+    |>(eqb_n_n j) normalize @sym_eq @(eqb_true_to_eq … Hni)
+    ]
+  |cases (true_or_false (eqb n j)) #Hnj >Hnj normalize
+    [>(eqb_n_n i) normalize @sym_eq @(eqb_true_to_eq … Hnj)
+    |>Hni >Hnj //
+    ]
+  ]
+qed.
+
+theorem injective_transpose : ∀i,j:nat. 
+  injective nat nat (transpose i j).
+// qed.
+
+theorem permut_transpose: ∀i,j,n. i ≤ n → j ≤ n → permut (transpose i j) n.
+#i #j #n #lein #lejn %
+  [#a #lean normalize cases (eqb a i) cases (eqb a j) normalize //
+  |#a #b #lean #lebn @(injective_to_injn (transpose i j) n) //
+  ]
+qed.
+
+theorem permut_fg: ∀f,g,n.
+  permut f n → permut g n → permut (λm.(f(g m))) n.
+#f #g #n * #permf1 #permf2 * #permg1 #permg2 %
+  [#i #lein @permf1 @permg1 @lein
+  |#a #b #lean #lebn #Heq @permg2 // @permf2 
+    [@permg1 @lean |@permg1 @lebn | //]
+  ]
+qed.   
+
+theorem permut_transpose_l: ∀f,m,i,j.i ≤ m → j ≤ m → 
+  permut f m → permut (λn.transpose i j (f n)) m.  
+#f #m #i #j #leim #lejm #permf @(permut_fg … permf) @permut_transpose // 
+qed.
+
+theorem permut_transpose_r: ∀f,m,i,j. i ≤ m → j ≤ m → 
+  permut f m → permut (λn.f (transpose i j n)) m.  
+#f #m #i #j #leim #lejm #permf @(permut_fg … permf) @permut_transpose // 
+qed.
+
+theorem eq_transpose : ∀i,j,k,n:nat. j≠i → i≠k → j≠k →
+  transpose i j n = transpose i k (transpose k j (transpose i k n)).
+#i #j #k #n #Hji #Hik #Hjk normalize
+cases (true_or_false (eqb n i)) #Hni >Hni normalize
+  [>(eqb_n_n k) normalize >(not_eq_to_eqb_false … Hji) 
+   >(not_eq_to_eqb_false … Hjk) % 
+  |cases (true_or_false (eqb n k)) #Hnk >Hnk normalize
+    [>(not_eq_to_eqb_false n j)
+      [2: @(not_to_not …Hjk) <(eqb_true_to_eq … Hnk) //]
+     >(not_eq_to_eqb_false … Hik) >(not_eq_to_eqb_false … i j)
+      [2: @(not_to_not … Hji) //] 
+     normalize >(eqb_n_n i) @(eqb_true_to_eq … Hnk)
+    |>Hnk normalize
+     cases (true_or_false (eqb n j)) #Hnj >Hnj normalize
+      [>(not_eq_to_eqb_false k i)[2: @(not_to_not … Hik) //] 
+       normalize >(eqb_n_n k) %
+      |>Hni >Hnk %
+      ]
+    ]
+  ]
+qed. 
+
+theorem permut_S_to_permut_transpose: ∀f,m.
+  permut f (S m) → permut (λn.transpose (f (S m)) (S m) (f n)) m.
+#f #m * #permf1 #permf2 %
+  [#i #leim normalize >(not_eq_to_eqb_false (f i) (f (S m))) normalize
+    [2: % #H @(absurd … (i= S m)) 
+      [@(permf2 … H) [@le_S //|//]  |@lt_to_not_eq @le_S_S //]
+    ]
+   cases(le_to_or_lt_eq … (permf1 … (le_S … leim))) #Hfi
+    [>(not_eq_to_eqb_false (f i) (S m)) [2:@lt_to_not_eq //]
+     normalize @le_S_S_to_le @Hfi
+    |>(eq_to_eqb_true …Hfi) normalize
+     cases(le_to_or_lt_eq … (permf1 … (le_n (S m)))) #H
+      [@le_S_S_to_le @H 
+      |@False_ind @(absurd (i= S m))
+        [@permf2 [@le_S // | //| //]
+        |@(not_to_not ? (S m ≤ m)) [// |@lt_to_not_le //]
+        ]
+      ]
+    ]
+  |#a #b #leam #lebm #H @permf2 
+    [@le_S //|@le_S //| @(injective_transpose … H)]
+  ]
+qed.
+        
+(* bounded bijectivity *)
+
+definition bijn : (nat → nat) → nat → Prop ≝
+λf,n.∀m:nat. m ≤ n → ex nat (λp. p ≤ n ∧ f p = m).
+
+theorem eq_to_bijn:  ∀f,g,n.
+  (∀i.i ≤ n → f i = g i) →  bijn f n → bijn g n.
+#f #g #n #H #bijf #i #lein cases (bijf … lein) #a * #lean #fa
+%{a} % // <fa @sym_eq @H //
+qed.
+
+theorem bijn_Sn_n: ∀f,n.
+  bijn f (S n) → f (S n) = S n → bijn f n.
+#f #n #bijf #fS #i #lein cases (bijf … (le_S … lein)) #a * #lean #fa
+cases (le_to_or_lt_eq … lean) #Hc
+  [%{a} % [@le_S_S_to_le @Hc |@fa]
+  |@False_ind @(absurd ?? (not_le_Sn_n n)) <fS //
+  ]
+qed.
+
+theorem bijn_n_Sn: ∀f,n.
+  bijn f n → f (S n) = S n → bijn f (S n).
+#f #n #bijf #fS #i #lein
+cases (le_to_or_lt_eq … lein) #Hi
+  [cases (bijf … (le_S_S_to_le … Hi)) #a * #lean #fa 
+   %{a} % [@le_S //|//]
+  |%{i} % //
+  ]
+qed.
+
+theorem bijn_fg: ∀f,g:nat→ nat.∀n:nat.
+  bijn f n → bijn g n → bijn (λp.f(g p)) n.
+#f #g #n #bijf #bijg #i #lein cases (bijf … lein) #a * #lean #ga
+cases (bijg … lean) #b * #lebn #gb %{b} % //
+qed.
+
+(*
+theorem bijn_to_injn: ∀f,n. bijn f n → injn f n.
+#f #n normalize #H #i #j #lein #lejn #eqf 
+cases (H … lein) #a * #lean #fa
+cases (H … lejn) #b * #lebn #fb
+cases (bijg … lean) #b * #lebn #gb %{b} % //
+qed.
+*)
+
+theorem bijn_transpose : ∀n,i,j. i ≤ n → j ≤ n →
+  bijn (transpose i j) n.
+#n #i #j #lein #lejn #a #lean
+cases (true_or_false (eqb a i)) #Hi
+  [%{j} % // >transpose_i_j_j @sym_eq @(eqb_true_to_eq … Hi)
+  |cases (true_or_false (eqb a j)) #Hj 
+    [%{i} % // >transpose_i_j_i @sym_eq @(eqb_true_to_eq … Hj)
+    |%{a} % // normalize >Hi >Hj %
+    ]
+  ]
+qed.  
+
+theorem bijn_transpose_r: ∀f,n,i,j. i ≤ n → j ≤ n →
+  bijn f n → bijn (λp.f (transpose i j p)) n.
+#f #n #i #j #lein #lejn #bijf @(bijn_fg f ?) /2/
+qed.
+
+theorem bijn_transpose_l: ∀f,n,i,j. i ≤ n → j ≤ n →
+  bijn f n → bijn (λp.transpose i j (f p)) n.
+#f #n #i #j #lein #lejn #bijf @(bijn_fg ? f) /2/
+qed.
+
+theorem permut_to_bijn: ∀n,f. permut f n → bijn f n.
+#n elim n 
+  [#f normalize * #H #H1 #m #lem0 %{0} % // 
+   @(le_n_O_elim … lem0) @sym_eq @le_n_O_to_eq @H //
+  |#m #Hind #f #permf 
+   @(eq_to_bijn (λp.
+      (transpose (f (S m)) (S m)) (transpose (f (S m)) (S m) (f p))) f)
+    [#i #lei @transpose_transpose
+    |@(bijn_fg (transpose (f (S m)) (S m)))
+      [cases permf #lef #_ @bijn_transpose [@lef // |//]
+      |@bijn_n_Sn 
+        [@Hind @permut_S_to_permut_transpose //
+        |normalize >(eqb_n_n (f (S m))) % 
+        ]
+      ]
+    ]
+  ]
+qed.
+
+let rec invert_permut n f m ≝
+  match eqb m (f n) with
+  [true ⇒ n
+  |false ⇒ 
+     match n with
+     [O ⇒ O
+     |(S p) ⇒ invert_permut p f m]].
+
+theorem invert_permut_f: ∀f:nat → nat. ∀n,m:nat.
+  m ≤ n → injn f n → invert_permut n f (f m) = m.
+#f #n #m #lenm elim lenm
+  [cases m normalize [>(eqb_n_n (f O)) //| #a >(eqb_n_n (f (S a))) //]
+  |#m0 #lem #H #H1 normalize 
+   >(not_eq_to_eqb_false (f m) (f (S m0))) 
+    [@H @injn_Sn_n //
+    |% #eqf @(absurd (m = S m0)) 
+      [@H1 [@le_S // |//|//] |@lt_to_not_eq @le_S_S //]
+    ]
+  ]
+qed.
+
+theorem injective_invert_permut: ∀f,n.
+  permut f n → injn (invert_permut n f) n.
+#f #n #permf #i #j #lein #lejn lapply (permut_to_bijn … permf) #bijf
+cases (bijf i lein) #a * #lean #fa
+cases (bijf j lejn) #b * #lebn #fb
+cases permf #_ #injf
+<fa <fb >(invert_permut_f … lean injf) >(invert_permut_f … lebn injf) //
+qed. 
+
+theorem permut_invert_permut: ∀f,n.
+  permut f n → permut (invert_permut n f) n.
+#f #n #permf % 
+  [#i #lein elim n normalize 
+    [cases (eqb i (f O)) %
+    |#n1 #Hind cases (eqb i (f (S n1))) [@le_n | normalize @le_S //]
+    ]
+  |@injective_invert_permut //
+  ]
+qed.
+
+theorem f_invert_permut: ∀f,n,m.
+  m ≤ n → permut f n → f (invert_permut n f m) = m.
+#f #n #m #lemn #permf lapply (permut_invert_permut … permf)
+* #Hle #Hinj cases permf #lef #injf @(injective_invert_permut … permf … lemn)
+  [@lef @Hle //
+  |@invert_permut_f [@Hle //| //]
+  ]
+qed.
+
+theorem permut_n_to_eq_n: ∀h,n.
+  permut h n → (∀m:nat. m < n → h m = m) → h n = n.
+#h #n #permh cases permh #leh #injh #eqh 
+lapply (permut_invert_permut … permh) * #Hle #Hinj
+cases (le_to_or_lt_eq … (Hle … (le_n n))) #Hc
+  [<(f_invert_permut … (le_n n) permh) in ⊢ (???%); @eq_f
+   <(f_invert_permut … (le_n n) permh) in ⊢ (??%?); @eqh @Hc
+  |<Hc in ⊢ (??%?); @(f_invert_permut h) //
+  ]
+qed.
+
+theorem permut_n_to_le: ∀h,k,n.
+k ≤ n → permut h n → (∀m.m < k → h m = m) → 
+  ∀j. k ≤ j → j ≤ n → k ≤ h j.
+#h #k #n #lekn * #leh #injh #H #j #lekj #lejn 
+cases (decidable_lt (h j) k) #Hh
+  [@False_ind @(absurd … lekj) @lt_to_not_le
+   cut (h j = j) 
+    [@injh [@(transitive_le … lekn) @lt_to_le // |@lejn|@H //]] #Hj 
+   <Hj //
+  |@not_lt_to_le //
+  ]
+qed.
diff --git a/matita/matita/lib/arithmetics/sigma_pi.ma b/matita/matita/lib/arithmetics/sigma_pi.ma
index 7e3fe19f0..8d2a5858a 100644
--- a/matita/matita/lib/arithmetics/sigma_pi.ma
+++ b/matita/matita/lib/arithmetics/sigma_pi.ma
@@ -186,3 +186,14 @@ theorem exp_sigma_l: ∀n,a,p,f.
   |>bigop_Sfalse [>bigop_Sfalse [@Hind|//] | //]
   ]
 qed.
+
+theorem exp_pi_l: ∀n,a,f. 
+  exp a n*(∏_{i < n}(f i)) = ∏_{i < n} (a*(f i)).
+#n #a #f elim n // #i #Hind >bigop_Strue // >bigop_Strue //
+<Hind <associative_times <associative_times @eq_f2 // normalize // 
+qed.
+
+theorem exp_pi_bc: ∀a,b,c,f. 
+  exp a (c-b)*(∏_{i ∈ [b,c[ }(f i)) = ∏_{i ∈ [b,c[ } (a*(f i)).
+#a #b #c #f @exp_pi_l 
+qed.
\ No newline at end of file
-- 
2.39.2