From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 23 Dec 2010 09:24:39 +0000 (+0000)
Subject: progress
X-Git-Tag: make_still_working~2627
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7ad16d18416a08382d62747fce4a0ac18ee557e0;p=helm.git

progress
---

diff --git a/matita/matita/lib/arithmetics/bigops.ma b/matita/matita/lib/arithmetics/bigops.ma
index 3211814db..03db53f7d 100644
--- a/matita/matita/lib/arithmetics/bigops.ma
+++ b/matita/matita/lib/arithmetics/bigops.ma
@@ -67,7 +67,7 @@ for @{'bigop ($b-$a) $op $nil (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
   
 notation "\big  [ op , nil ]_{ ident j ∈ [a,b[ } f"
   with precedence 80
-for @{'bigop ($b-$a) $op $nil (λ${ident j}.((λ${ident j}.$true) (${ident j}+$a)))
+for @{'bigop ($b-$a) $op $nil (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.  
  
 (* notation "\big  [ op , nil ]_{( term 50) a ≤ ident j < b | p } f"
@@ -142,13 +142,29 @@ a ≤ b → b ≤ c →
       \big[op,nil]_{i ∈ [a,b[ |p i}(f i).
 #a #b # c #p #B #nil #op #f #leab #lebc 
 >(plus_minus_m_m (c-a) (b-a)) in ⊢ (??%?) /2/
->minus_minus >(commutative_plus a) <plus_minus_m_m //
+>minus_plus >(commutative_plus a) <plus_minus_m_m //
 >bigop_sum (cut (∀i. b -a ≤ i → i+a = i-(b-a)+b))
   [#i #lei >plus_minus // <plus_minus1 
      [@eq_f @sym_eq @plus_to_minus /2/ | /2/]] 
 #H @same_bigop #i #ltic @leb_elim normalize // #lei <H //
 qed.   
 
+theorem bigop_a: ∀a,b,B.∀nil.∀op:Aop B nil.∀f:nat→B. a ≤ b →
+\big[op,nil]_{i∈[a,S b[ }(f i) = 
+  op (\big[op,nil]_{i ∈ [a,b[ }(f (S i))) (f a).
+#a #b #B #nil #op #f #leab 
+>(bigop_sumI a (S a) (S b)) [|@le_S_S //|//] @eq_f2 
+  [@same_bigop // |<minus_Sn_n normalize @nilr]
+qed.
+  
+theorem bigop_0: ∀n,B.∀nil.∀op:Aop B nil.∀f:nat→B.
+\big[op,nil]_{i < S n}(f i) = 
+  op (\big[op,nil]_{i < n}(f (S i))) (f 0).
+#n #B #nil #op #f 
+<bigop_I >bigop_a [|//] @eq_f2 [|//] <minus_n_O 
+@same_bigop //
+qed.    
+
 theorem bigop_prod: ∀k1,k2,p1,p2,B.∀nil.∀op:Aop B nil.∀f: nat →nat → B.
 \big[op,nil]_{x<k1|p1 x}(\big[op,nil]_{i<k2|p2 x i}(f x i)) =
   \big[op,nil]_{i<k1*k2|andb (p1 (div i k2)) (p2 (div i k2) (i \mod k2))}
@@ -169,7 +185,19 @@ record ACop (A:Type[0]) (nil:A) : Type[0] ≝
   {aop :> Aop A nil; 
    comm: ∀a,b.aop a b = aop b a
   }.
-  
+ 
+lemma bigop_op: ∀k,p,B.∀nil.∀op:ACop B nil.∀f,g: nat → B.
+op (\big[op,nil]_{i<k|p i}(f i)) (\big[op,nil]_{i<k|p i}(g i)) =
+  \big[op,nil]_{i<k|p i}(op (f i) (g i)).
+#k #p #B #nil #op #f #g (elim k) [normalize @nill]
+-k #k #Hind (cases (true_or_false (p k))) #H
+  [>bigop_Strue // >bigop_Strue // >bigop_Strue //
+   <assoc <assoc in ⊢ (???%) @eq_f >assoc >comm in ⊢ (??(????%?)?) 
+   <assoc @eq_f @Hind
+  |>bigop_Sfalse // >bigop_Sfalse // >bigop_Sfalse //
+  ]
+qed.
+
 lemma bigop_diff: ∀p,B.∀nil.∀op:ACop B nil.∀f:nat → B.∀i,n.
   i < n → p i = true →
   \big[op,nil]_{x<n|p x}(f x)=
@@ -265,7 +293,30 @@ theorem bigop_iso: ∀n1,n2,p1,p2,B.∀nil.∀op:ACop B nil.∀f1,f2.
   ]
 qed.
 
-(* Sigma e Pi *)
+(* distributivity *)
+
+record Dop (A:Type[0]) (nil:A): Type[0] ≝
+  {sum : ACop A nil; 
+   prod: A → A →A;
+   null: \forall a. prod a nil = nil; 
+   distr: ∀a,b,c:A. prod a (sum b c) = sum (prod a b) (prod a c)
+  }.
+  
+theorem bigop_distr: ∀n,p,B,nil.∀R:Dop B nil.\forall f,a.
+  let aop \def  sum B nil R in
+  let mop \def prod B nil R in
+  mop a \big[aop,nil]_{i<n|p i}(f i) = 
+   \big[aop,nil]_{i<n|p i}(mop a (f i)).
+#n #p #B #nil #R #f #a normalize (elim n) [@null]
+#n #Hind (cases (true_or_false (p n))) #H
+  [>bigop_Strue // >bigop_Strue // >(distr B nil R) >Hind //
+  |>bigop_Sfalse // >bigop_Sfalse //
+  ]
+qed.
+  
+(* Sigma e Pi 
+
+
 notation "Σ_{ ident i < n | p } f"
   with precedence 80
 for @{'bigop $n plus 0 (λ${ident i}.p) (λ${ident i}. $f)}.
@@ -301,7 +352,8 @@ notation "Π_{ ident j ∈ [a,b[ | p } f"
   with precedence 80
 for @{'bigop ($b-$a) times 1 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
- 
+
+*)
 (*
     
 definition p_ord_times \def
@@ -720,44 +772,7 @@ cut (O < p)
 ]
 qed.
     
-(*distributive property for iter_p_gen*)
-theorem distributive_times_plus_iter_p_gen: \forall A:Type.
-\forall plusA: A \to A \to A. \forall basePlusA: A.
-\forall timesA: A \to A \to A. 
-\forall n:nat. \forall k:A. \forall p:nat \to bool. \forall g:nat \to A.
-(symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  basePlusA) = a) \to
-(symmetric A timesA) \to (distributive A timesA plusA) \to
-(\forall a:A. (timesA a basePlusA) = basePlusA)
- 
-  \to
 
-((timesA k (iter_p_gen n p A g basePlusA plusA)) = 
- (iter_p_gen n p A (\lambda i:nat.(timesA k (g i))) basePlusA plusA)).
-intros.
-elim n
-[ simplify.
-  apply H5
-| cut( (p n1) = true \lor (p n1) = false)
-  [ elim Hcut
-    [ rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H7).
-      rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H7) in \vdash (? ? ? %).
-      rewrite > (H4).
-      rewrite > (H3 k (g n1)).
-      apply eq_f.
-      assumption
-    | rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H7).
-      rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H7) in \vdash (? ? ? %).
-      assumption
-    ]
-  | elim ((p n1))
-    [ left.
-      reflexivity
-    | right.
-      reflexivity
-    ]
-  ]
-]
-qed.
 
 theorem iter_p_gen_2_eq: 
 \forall A:Type.
diff --git a/matita/matita/lib/arithmetics/binomial.ma b/matita/matita/lib/arithmetics/binomial.ma
index 414b71a15..9397f7b4d 100644
--- a/matita/matita/lib/arithmetics/binomial.ma
+++ b/matita/matita/lib/arithmetics/binomial.ma
@@ -9,7 +9,7 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "arithmetics/bigops.ma".
+include "arithmetics/sigma_pi.ma".
 include "arithmetics/primes.ma".
 
 (* binomial coefficient *)
@@ -27,10 +27,10 @@ theorem bc_n_O: ∀n. bc n O = 1.
 qed.
 
 theorem fact_minus: ∀n,k. k < n → 
-  (n-k)*(n - S k)! = (n - k)!.
+  (n - S k)!*(n-k) = (n - k)!.
 #n #k (cases n)
   [#ltO @False_ind /2/
-  |#l #ltl >minus_Sn_m [>commutative_times //|@le_S_S_to_le //]
+  |#l #ltl >(minus_Sn_m k) [// |@le_S_S_to_le //]
   ]
 qed.
 
@@ -38,201 +38,89 @@ theorem bc2 : ∀n.
 ∀k. k ≤n → k!*(n-k)! ∣ n!.
 #n (elim n) 
   [#k #lek0 <(le_n_O_to_eq ? lek0) //
-  |#m #Hind #k generalize in match H1;cases k
-     [intro;simplify in ⊢ (? (? ? (? %)) ?);simplify in ⊢ (? (? % ?) ?);
-      rewrite > sym_times;rewrite < times_n_SO;apply reflexive_divides
-     |intro;elim (decidable_eq_nat n2 n1)
-        [rewrite > H3;rewrite < minus_n_n;
-         rewrite > times_n_SO in ⊢ (? ? %);apply reflexive_divides
-        |lapply (H n2)
-           [lapply (H (n1 - (S n2)))
-              [change in ⊢ (? ? %) with ((S n1)*n1!);
-               rewrite > (plus_minus_m_m n1 n2) in ⊢ (? ? (? (? %) ?))
-                 [rewrite > sym_plus;
-                  change in ⊢ (? ? (? % ?)) with ((S n2) + (n1 - n2));
-                  rewrite > sym_times in \vdash (? ? %);
-                  rewrite > distr_times_plus in ⊢ (? ? %);
-                  simplify in ⊢ (? (? ? (? %)) ?);
-                  apply divides_plus
-                    [rewrite > sym_times;
-                     change in ⊢ (? (? ? %) ?) with ((S n2)*n2!);
-                     rewrite > sym_times in ⊢ (? (? ? %) ?);
-                     rewrite < assoc_times;
-                     apply divides_times
-                       [rewrite > sym_times;assumption
-                       |apply reflexive_divides]
-                    |rewrite < fact_minus in ⊢ (? (? ? %) ?)
-                       [rewrite > sym_times in ⊢ (? (? ? %) ?);
-                        rewrite < assoc_times;
-                        apply divides_times
-                          [rewrite < eq_plus_minus_minus_minus in Hletin1;
-                             [rewrite > sym_times;rewrite < minus_n_n in Hletin1;
-                              rewrite < plus_n_O in Hletin1;assumption
-                             |lapply (le_S_S_to_le ? ? H2);
-                              elim (le_to_or_lt_eq ? ? Hletin2);
-                                [assumption
-                                |elim (H3 H4)]
-                             |constructor 1]
-                          |apply reflexive_divides]
-                       |lapply (le_S_S_to_le ? ? H2);
-                        elim (le_to_or_lt_eq ? ? Hletin2);
-                          [assumption
-                          |elim (H3 H4)]]]
-                 |apply le_S_S_to_le;assumption]
-              |apply le_minus_m;apply le_S_S_to_le;assumption]
-           |apply le_S_S_to_le;assumption]]]]
-qed.                      
-    
-theorem bc1: \forall n.\forall k. k < n \to bc (S n) (S k) = (bc n k) + (bc n (S k)). 
-intros.unfold bc.
-rewrite > (lt_to_lt_to_eq_div_div_times_times ? ? (S k)) in ⊢ (? ? ? (? % ?))
-  [rewrite > sym_times in ⊢ (? ? ? (? (? ? %) ?)). 
-   rewrite < assoc_times in ⊢ (? ? ? (? (? ? %) ?)).
-   rewrite > (lt_to_lt_to_eq_div_div_times_times ? ? (n - k)) in ⊢ (? ? ? (? ? %))
-    [rewrite > assoc_times in ⊢ (? ? ? (? ? (? ? %))).
-     rewrite > sym_times in ⊢ (? ? ? (? ? (? ? (? ? %)))).
-     rewrite > fact_minus
-      [rewrite < eq_div_plus
-        [rewrite < distr_times_plus.
-         simplify in ⊢ (? ? ? (? (? ? %) ?)).
-         rewrite > sym_plus in ⊢ (? ? ? (? (? ? (? %)) ?)).
-         rewrite < plus_minus_m_m
-          [rewrite > sym_times in ⊢ (? ? ? (? % ?)).
-           reflexivity
-          |apply lt_to_le.
-           assumption
-          ]
-        |rewrite > (times_n_O O).
-         apply lt_times;apply lt_O_fact
-        |change in ⊢ (? (? % ?) ?) with ((S k)*k!);
-         rewrite < sym_times in ⊢ (? ? %);
-         rewrite > assoc_times;apply divides_times
-           [apply reflexive_divides
-           |apply bc2;apply le_S_S_to_le;constructor 2;assumption]
-        |rewrite < fact_minus
-           [rewrite > sym_times in ⊢ (? (? ? %) ?);rewrite < assoc_times;
-            apply divides_times
-              [apply bc2;assumption
-              |apply reflexive_divides]
-           |assumption]]
-     |assumption]
-  |apply lt_to_lt_O_minus;assumption
-  |rewrite > (times_n_O O).
-   apply lt_times;apply lt_O_fact]
-|apply lt_O_S
-|rewrite > (times_n_O O).
- apply lt_times;apply lt_O_fact]
-qed.
-
-theorem lt_O_bc: \forall n,m. m \le n \to O < bc n m.
-intro.elim n
-  [apply (le_n_O_elim ? H).
-   simplify.apply le_n
-  |elim (le_to_or_lt_eq ? ? H1)
-    [generalize in match H2.cases m;intro
-      [rewrite > bc_n_O.apply le_n
-      |rewrite > bc1
-        [apply (trans_le ? (bc n1 n2))
-          [apply H.apply le_S_S_to_le.apply lt_to_le.assumption
-          |apply le_plus_n_r
-          ]
-        |apply le_S_S_to_le.assumption
-        ]
+  |#m #Hind #k (cases k) normalize //
+     #c #lec cases (le_to_or_lt_eq … (le_S_S_to_le …lec))
+    [#ltcm 
+     cut (m-(m-(S c)) = S c) [@plus_to_minus @plus_minus_m_m //] #eqSc     
+     lapply (Hind c (le_S_S_to_le … lec)) #Hc
+     lapply (Hind (m - (S c)) ?) [@le_plus_to_minus //] >eqSc #Hmc
+     >(plus_minus_m_m m c) in ⊢ (??(??(?%))) [|@le_S_S_to_le //]
+     >commutative_plus >(distributive_times_plus ? (S c))
+     @divides_plus
+      [>associative_times >(commutative_times (S c))
+       <associative_times @divides_times //
+      |<(fact_minus …ltcm) in ⊢ (?(??%)?) 
+       <associative_times @divides_times //
+       >commutative_times @Hmc
       ]
-    |rewrite > H2.
-     rewrite > bc_n_n.
-     apply le_n
+    |#eqcm >eqcm <minus_n_n <times_n_1 // 
     ]
   ]
 qed.
-
-theorem exp_plus_sigma_p:\forall a,b,n.
-exp (a+b) n = sigma_p (S n) (\lambda k.true) 
-  (\lambda k.(bc n k)*(exp a (n-k))*(exp b k)).
-intros.elim n
-  [simplify.reflexivity
-  |simplify in ⊢ (? ? % ?).
-   rewrite > true_to_sigma_p_Sn
-    [rewrite > H;rewrite > sym_times in ⊢ (? ? % ?);
-     rewrite > distr_times_plus in ⊢ (? ? % ?);
-     rewrite < minus_n_n in ⊢ (? ? ? (? (? (? ? (? ? %)) ?) ?));
-     rewrite > sym_times in ⊢ (? ? (? % ?) ?);
-     rewrite > sym_times in ⊢ (? ? (? ? %) ?);
-     rewrite > distributive_times_plus_sigma_p in ⊢ (? ? (? % ?) ?);
-     rewrite > distributive_times_plus_sigma_p in ⊢ (? ? (? ? %) ?);
-     rewrite > true_to_sigma_p_Sn in ⊢ (? ? (? ? %) ?)
-       [rewrite < assoc_plus;rewrite < sym_plus in ⊢ (? ? (? % ?) ?);
-        rewrite > assoc_plus;
-        apply eq_f2
-          [rewrite > sym_times;rewrite > assoc_times;autobatch paramodulation
-          |rewrite > (sigma_p_gi ? ? O);
-            [rewrite < (eq_sigma_p_gh ? S pred n1 (S n1) (λx:nat.true)) in ⊢ (? ? (? (? ? %) ?) ?)
-               [rewrite > (sigma_p_gi ? ? O) in ⊢ (? ? ? %);
-                  [rewrite > assoc_plus;apply eq_f2
-                     [autobatch paramodulation; 
-                     |rewrite < sigma_p_plus_1;
-                      rewrite < (eq_sigma_p_gh ? S pred n1 (S n1) (λx:nat.true)) in \vdash (? ? ? %);
-                        [apply eq_sigma_p
-                           [intros;reflexivity
-                           |intros;rewrite > sym_times;rewrite > assoc_times;
-                            rewrite > sym_times in ⊢ (? ? (? (? ? %) ?) ?);
-                            rewrite > assoc_times;rewrite < assoc_times in ⊢ (? ? (? (? ? %) ?) ?);
-                            rewrite > sym_times in ⊢ (? ? (? (? ? (? % ?)) ?) ?);
-                            change in ⊢ (? ? (? (? ? (? % ?)) ?) ?) with (exp a (S (n1 - S x)));
-                            rewrite < (minus_Sn_m ? ? H1);rewrite > minus_S_S;
-                            rewrite > sym_times in \vdash (? ? (? ? %) ?);
-                            rewrite > assoc_times; 
-                            rewrite > sym_times in ⊢ (? ? (? ? (? ? %)) ?);
-                            change in \vdash (? ? (? ? (? ? %)) ?) with (exp b (S x));
-                            rewrite > assoc_times in \vdash (? ? (? ? %) ?);
-                            rewrite > sym_times in \vdash (? ? (? % ?) ?);
-                            rewrite > sym_times in \vdash (? ? (? ? %) ?);
-                            rewrite > assoc_times in \vdash (? ? ? %);
-                            rewrite > sym_times in \vdash (? ? ? %);
-                            rewrite < distr_times_plus;
-                            rewrite > sym_plus;rewrite < bc1;
-                              [reflexivity|assumption]]
-                        |intros;simplify;reflexivity
-                        |intros;simplify;reflexivity
-                        |intros;apply le_S_S;assumption
-                        |intros;reflexivity
-                        |intros 2;elim j
-                            [simplify in H2;destruct H2
-                            |simplify;reflexivity]
-                        |intro;elim j
-                            [simplify in H2;destruct H2
-                            |simplify;apply le_S_S_to_le;assumption]]]
-                  |apply le_S_S;apply le_O_n
-                  |reflexivity]
-               |intros;simplify;reflexivity
-               |intros;simplify;reflexivity
-               |intros;apply le_S_S;assumption
-               |intros;reflexivity
-               |intros 2;elim j
-                  [simplify in H2;destruct H2
-                  |simplify;reflexivity]
-               |intro;elim j
-                  [simplify in H2;destruct H2
-                  |simplify;apply le_S_S_to_le;assumption]]
-            |apply le_S_S;apply le_O_n
-            |reflexivity]]
-      |reflexivity]
-   |reflexivity]]
+           
+theorem bc1: ∀n.∀k. k < n → 
+  bc (S n) (S k) = (bc n k) + (bc n (S k)).
+#n #k #ltkn > bceq >(bceq n) >(bceq n (S k))
+>(div_times_times ?? (S k)) in ⊢ (???(?%?)) 
+  [|>(times_n_O 0) @lt_times // | //]
+>associative_times in ⊢ (???(?(??%)?))
+>commutative_times in ⊢ (???(?(??(??%))?))
+<associative_times in ⊢ (???(?(??%)?))
+>(div_times_times ?? (n - k)) in ⊢ (???(??%))  
+  [|>(times_n_O 0) @lt_times // 
+   |@(le_plus_to_le_r k ??) <plus_minus_m_m /2/]
+>associative_times in ⊢ (???(??(??%)))
+>fact_minus // <plus_div 
+  [<distributive_times_plus
+   >commutative_plus in ⊢ (???%) <plus_n_Sm <plus_minus_m_m [|/2/] @refl
+  |<fact_minus // <associative_times @divides_times // @(bc2 n (S k)) //
+  |>associative_times >(commutative_times (S k))
+   <associative_times @divides_times // @bc2 /2/
+  |>(times_n_O 0) @lt_times [@(le_1_fact (S k)) | //]
+  ]
 qed.
 
-theorem exp_S_sigma_p:\forall a,n.
-exp (S a) n = sigma_p (S n) (\lambda k.true) (\lambda k.(bc n k)*(exp a (n-k))).
-intros.
-rewrite > plus_n_SO.
-rewrite > exp_plus_sigma_p.
-apply eq_sigma_p;intros
-  [reflexivity
-  |rewrite < exp_SO_n.
-   rewrite < times_n_SO.
-   reflexivity
+theorem lt_O_bc: ∀n,m. m ≤ n → O < bc n m.
+#n (elim n) 
+  [#m #lemO @(le_n_O_elim ? lemO) //
+  |-n #n #Hind #m (cases m) //
+   #m #lemn cases(le_to_or_lt_eq … (le_S_S_to_le …lemn)) //
+   #ltmn >bc1 // >(plus_O_n 0) @lt_plus @Hind /2/
   ]
+qed. 
+
+theorem binomial_law:∀a,b,n.
+  (a+b)^n = Σ_{k < S n}((bc n k)*(a^(n-k))*(b^k)).
+#a #b #n (elim n) //
+-n #n #Hind normalize in ⊢ (? ? % ?).
+>bigop_Strue // >Hind >distributive_times_plus 
+<(minus_n_n (S n)) <commutative_times <(commutative_times b)
+(* hint??? *)
+>(bigop_distr ???? natDop ? a) >(bigop_distr ???? natDop ? b)
+>bigop_Strue in ⊢ (??(??%)?) // <associative_plus 
+<commutative_plus in ⊢ (??(? % ?) ?) >associative_plus @eq_f2
+  [<minus_n_n >bc_n_n >bc_n_n normalize //
+  |>bigop_0 >associative_plus >commutative_plus in ⊢ (??(??%)?) 
+   <associative_plus >bigop_0 // @eq_f2 
+    [>(bigop_op n ??? natACop) @same_bigop //
+     #i #ltin #_ <associative_times >(commutative_times b)
+     >(associative_times ?? b) <(distributive_times_plus_r (b^(S i)))
+     @eq_f2 // <associative_times >(commutative_times a) 
+     >associative_times cut(∀n.a*a^n = a^(S n)) [#n @commutative_times] #H
+     >H <minus_Sn_m // <(distributive_times_plus_r (a^(n-i)))
+     @eq_f2 // @sym_eq >commutative_plus @bc1 //
+    |>bc_n_O >bc_n_O normalize //
+    ]
+  ]
+qed.
+     
+theorem exp_S_sigma_p:∀a,n.
+(S a)^n = Σ_{k < S n}((bc n k)*a^(n-k)).
+#a #n cut (S a = a + 1) // #H >H
+>binomial_law @same_bigop //
 qed.
 
+(*
 theorem exp_Sn_SSO: \forall n. exp (S n) 2 = S((exp n 2) + 2*n).
 intros.simplify.
 rewrite < times_n_SO.
@@ -241,5 +129,5 @@ rewrite < sym_times.simplify.
 rewrite < assoc_plus.
 rewrite < sym_plus.
 reflexivity.
-qed.
+qed. *)
 
diff --git a/matita/matita/lib/arithmetics/chinese_reminder.ma b/matita/matita/lib/arithmetics/chinese_reminder.ma
new file mode 100644
index 000000000..0837e429e
--- /dev/null
+++ b/matita/matita/lib/arithmetics/chinese_reminder.ma
@@ -0,0 +1,132 @@
+(*
+    ||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/congruence.ma".
+
+theorem congruent_ab: ∀m,n,a,b:nat. O < n → O < m → 
+ gcd n m = 1 → ∃x.x ≅_{m} a ∧ x ≅_{n} b.
+#m #n #a #b #posn #posm #pnm
+cut (∃c,d.c*n - d*m = 1 ∨ d*m - c*n = 1) [<pnm @eq_minus_gcd]
+* #c * #d * #H
+  [(* first case *)
+   @(ex_intro nat ? ((a+b*m)*c*n-b*d*m)) %
+    [(* congruent to a *)
+     cut (c*n = d*m + 1)
+      [@minus_to_plus // @(transitive_le … (le_n_Sn …)) 
+       @(lt_minus_to_plus_r 0) //] -H #H
+     >associative_times >H <(commutative_plus ? (d*m))
+     >distributive_times_plus <times_n_1 >associative_plus
+     <associative_times <distributive_times_plus_r 
+     <commutative_plus <plus_minus
+       [@(eq_times_plus_to_congruent … posm) //
+       |applyS monotonic_le_times_r @(transitive_le ? ((a+b*m)*d)) // 
+        applyS monotonic_le_times_r apply (transitive_le … (b*m)) /2/
+       ]
+    |(* congruent to b *)
+     -pnm (cut (d*m = c*n-1))
+       [@sym_eq @plus_to_minus >commutative_plus 
+        @minus_to_plus // @(transitive_le … (le_n_Sn …)) 
+     @(lt_minus_to_plus_r 0) //] #H1
+     >(associative_times b d) >H1 >distributive_times_minus 
+     <associative_times <minus_minus
+       [@(eq_times_plus_to_congruent … posn) //
+       |applyS monotonic_le_times_r >commutative_times
+        @monotonic_le_times_r @(transitive_le ? (m*b)) /2/
+       |applyS monotonic_le_times_r @le_plus_to_minus // 
+       ]
+    ]
+  |(* and now the symmetric case; the price to pay for working
+      in nat instead than Z *)
+   @(ex_intro nat ? ((b+a*n)*d*m-a*c*n)) %
+    [(* congruent to a *)
+     cut (c*n = d*m - 1) 
+       [@sym_eq @plus_to_minus >commutative_plus @minus_to_plus // @(transitive_le … (le_n_Sn …)) 
+        @(lt_minus_to_plus_r 0) //] #H1
+     >(associative_times a c) >H1
+     >distributive_times_minus
+     <minus_minus
+      [@(eq_times_plus_to_congruent … posm) //
+      |<associative_times applyS monotonic_le_times_r
+       >commutative_times @monotonic_le_times_r 
+       @(transitive_le ? (n*a)) /2/
+      |@monotonic_le_times_r <H @le_plus_to_minus //
+      ]
+    |(* congruent to b *)
+     cut (d*m = c*n + 1)
+      [@minus_to_plus // @(transitive_le … (le_n_Sn …)) 
+       @(lt_minus_to_plus_r 0) //] -H #H
+     >associative_times >H
+     >(commutative_plus (c*n))
+     >distributive_times_plus <times_n_1
+     <associative_times >associative_plus 
+     <distributive_times_plus_r <commutative_plus <plus_minus
+      [@(eq_times_plus_to_congruent … posn) //
+      |applyS monotonic_le_times_r @(transitive_le ? (c*(b+n*a))) // 
+       <commutative_times @monotonic_le_times_r
+       @(transitive_le ? (n*a)) /2/
+      ]
+    ]
+  ]
+qed.
+       
+theorem congruent_ab_lt: ∀m,n,a,b. O < n → O < m → 
+gcd n m = 1 → ∃x.x ≅_{m} a ∧ x ≅_{n} b ∧ x < m*n.
+#m #n #a #b #posn #posm #pnm
+cases(congruent_ab m n a b posn posm pnm) #x * #cxa #cxb
+@(ex_intro ? ? (x \mod (m*n))) % 
+  [% 
+    [@(transitive_congruent m ? x) // 
+     @sym_eq >commutative_times @congruent_n_mod_times //
+    |@(transitive_congruent n ? x) // 
+     @sym_eq @congruent_n_mod_times //
+    ]
+  |@lt_mod_m_m >(times_n_O 0) @lt_times //
+  ]
+qed.
+
+definition cr_pair ≝ λn,m,a,b. 
+min (n*m) 0 (λx. andb (eqb (x \mod n) a) (eqb (x \mod m) b)).
+
+example cr_pair1: cr_pair 2 3 O O = O.
+// qed.
+
+example cr_pair2: cr_pair 2 3 1 0 = 3.
+// qed.
+
+example cr_pair3: cr_pair 2 3 1 2 = 5.
+// qed.
+
+example cr_pair4: cr_pair 5 7 3 2 = 23.
+// qed.
+
+example cr_pair5: cr_pair 3 7 0 4 = ?.
+normalize
+// qed.
+
+theorem mod_cr_pair : ∀m,n,a,b. a < m → b < n → gcd n m = 1 → 
+(cr_pair m n a b) \mod m = a ∧ (cr_pair m n a b) \mod n = b.
+#m #n #a #b #ltam #ltbn #pnm 
+cut (andb (eqb ((cr_pair m n a b) \mod m) a) 
+         (eqb ((cr_pair m n a b) \mod n) b) = true)
+  [@f_min_true cases(congruent_ab_lt m n a b ?? pnm)
+    [#x * * #cxa #cxb #ltx @(ex_intro ?? x) % /2/
+     >eq_to_eqb_true 
+      [>eq_to_eqb_true // <(lt_to_eq_mod …ltbn) //
+      |<(lt_to_eq_mod …ltam) //
+      ]
+    |@(le_to_lt_to_lt … ltbn) //
+    |@(le_to_lt_to_lt … ltam) //
+    ]
+  |#H >(eqb_true_to_eq … (andb_true_l … H)) >(eqb_true_to_eq … (andb_true_r … H)) /2/
+  ]
+qed.
diff --git a/matita/matita/lib/arithmetics/congruence.ma b/matita/matita/lib/arithmetics/congruence.ma
index e8f8a7732..d1afc19ee 100644
--- a/matita/matita/lib/arithmetics/congruence.ma
+++ b/matita/matita/lib/arithmetics/congruence.ma
@@ -81,7 +81,7 @@ theorem congruent_to_divides: ∀n,m,p:nat.O < p →
 #n #m #p #posp #congnm @(quotient ? ? ((n / p)-(m / p)))
 >commutative_times >(div_mod n p) in ⊢ (??%?)
 >(div_mod m p) in ⊢ (??%?) <(commutative_plus (m \mod p))
-<congnm <(minus_minus ? (n \mod p)) <minus_plus_m_m //
+<congnm <(minus_plus ? (n \mod p)) <minus_plus_m_m //
 qed.
 
 theorem mod_times: ∀n,m,p:nat. O < p → 
diff --git a/matita/matita/lib/arithmetics/div_and_mod.ma b/matita/matita/lib/arithmetics/div_and_mod.ma
index cf19b8203..4044695d2 100644
--- a/matita/matita/lib/arithmetics/div_and_mod.ma
+++ b/matita/matita/lib/arithmetics/div_and_mod.ma
@@ -367,30 +367,11 @@ split
 ]
 qed. *)
 
-theorem le_plus_to_minus_r: ∀a,b,c. a + b ≤ c → a ≤ c -b.
-#a #b #c #H @(le_plus_to_le_r … b) /2/
-qed.
-
-theorem le_minus_to_plus_r: ∀a,b,c. c ≤ b → a ≤ b - c → a + c ≤ b.
-#a #b #c #Hlecb #H >(plus_minus_m_m … Hlecb) /2/
-qed.
-
-theorem lt_minus_to_plus: ∀a,b,c. a - b < c → a < c + b.
-#a #b #c #H @not_le_to_lt 
-@(not_to_not … (lt_to_not_le …H)) /2/
-qed.
-
-theorem lt_minus_to_plus_r: ∀a,b,c. c ≤ a → 
-  a < b + c → a - c < b.
-#a #b #c #lea #H @not_le_to_lt 
-@(not_to_not … (lt_to_not_le …H)) /2/
-qed. 
-
 theorem lt_to_le_times_to_lt_S_to_div: ∀a,c,b:nat.
 O < b → (b*c) ≤ a → a < (b*(S c)) → a/b = c.
 #a #c #b #posb#lea #lta
 @(div_mod_spec_to_eq … (a-b*c) (div_mod_spec_div_mod … posb …))
-@div_mod_spec_intro [@lt_minus_to_plus_r // |/2/]
+@div_mod_spec_intro [@lt_plus_to_minus // |/2/]
 qed.
 
 theorem div_times_times: ∀a,b,c:nat. O < c → O < b → 
diff --git a/matita/matita/lib/arithmetics/gcd.ma b/matita/matita/lib/arithmetics/gcd.ma
index 86b0600be..104b59862 100644
--- a/matita/matita/lib/arithmetics/gcd.ma
+++ b/matita/matita/lib/arithmetics/gcd.ma
@@ -157,8 +157,8 @@ qed.
 
 (* a particular case of the previous theorem, with c=1 *)
 theorem divides_d_gcd: ∀m,n,d. 
- d ∣ m → d ∣ n → d ∣ gcd n m. 
-/2/ (* bello *)
+ d ∣ m → d ∣ n → d ∣ gcd n m.
+#m #n #d #divdn #divdn applyS (divides_d_times_gcd m n d 1) //
 qed.
 
 theorem eq_minus_gcd_aux: ∀p,m,n.O < n → n ≤ m →  n ≤ p →
@@ -184,13 +184,13 @@ theorem eq_minus_gcd_aux: ∀p,m,n.O < n → n ≤ m →  n ≤ p →
        <commutative_plus >distributive_times_plus_r 
        >(div_mod m n) in ⊢(? ? (? % ?) ?)
        >associative_times <commutative_plus >distributive_times_plus
-       <minus_minus <commutative_plus <plus_minus //
+       <minus_plus <commutative_plus <plus_minus //
       |(* second case *)
         <H @(ex_intro ?? (b+a*(m / n))) @(ex_intro ?? a) %1
         >distributive_times_plus_r
         >(div_mod m n) in ⊢ (? ? (? ? %) ?)
         >distributive_times_plus >associative_times
-        <minus_minus <commutative_plus <plus_minus //
+        <minus_plus <commutative_plus <plus_minus //
       ]
     ]
   ]
diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index 7ca90dcb2..6b3a1a19b 100644
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -913,9 +913,35 @@ theorem le_minus_to_plus: ∀n,m,p. n-m ≤ p → n≤ p+m.
   [|@le_plus_minus_m_m | @monotonic_le_plus_l // ]
 qed.
 
+theorem le_minus_to_plus_r: ∀a,b,c. c ≤ b → a ≤ b - c → a + c ≤ b.
+#a #b #c #Hlecb #H >(plus_minus_m_m … Hlecb) /2/
+qed.
+
 theorem le_plus_to_minus: ∀n,m,p. n ≤ p+m → n-m ≤ p.
 #n #m #p #lep /2/ qed.
 
+theorem le_plus_to_minus_r: ∀a,b,c. a + b ≤ c → a ≤ c -b.
+#a #b #c #H @(le_plus_to_le_r … b) /2/
+qed.
+
+theorem lt_minus_to_plus: ∀a,b,c. a - b < c → a < c + b.
+#a #b #c #H @not_le_to_lt 
+@(not_to_not … (lt_to_not_le …H)) /2/
+qed.
+
+theorem lt_minus_to_plus_r: ∀a,b,c. a < b - c → a + c < b.
+#a #b #c #H @not_le_to_lt @(not_to_not … (le_plus_to_minus …))
+@lt_to_not_le //
+qed.
+
+theorem lt_plus_to_minus: ∀n,m,p. m ≤ n → n < p+m → n-m < p.
+#n #m #p #lenm #H normalize <minus_Sn_m // @le_plus_to_minus //
+qed.
+
+theorem lt_plus_to_minus_r: ∀a,b,c. a + b < c → a < c - b.
+#a #b #c #H @le_plus_to_minus_r //
+qed. 
+
 theorem monotonic_le_minus_r: 
 ∀p,q,n:nat. q ≤ p → n-p ≤ n-q.
 #p #q #n #lepq @le_plus_to_minus
@@ -936,7 +962,7 @@ theorem distributive_times_minus: distributive ? times minus.
   @eq_f (applyS plus_minus_m_m) /2/
 qed.
 
-theorem minus_minus: ∀n,m,p. n-m-p = n -(m+p).
+theorem minus_plus: ∀n,m,p. n-m-p = n -(m+p).
 #n #m #p 
 cases (decidable_le (m+p) n) #Hlt
   [@plus_to_minus @plus_to_minus <associative_plus
@@ -946,6 +972,19 @@ cases (decidable_le (m+p) n) #Hlt
   ]
 qed.
 
+(*
+theorem plus_minus: ∀n,m,p. p ≤ m → (n+m)-p = n +(m-p).
+#n #m #p #lepm @plus_to_minus >(commutative_plus p)
+>associative_plus <plus_minus_m_m //
+qed.  *)
+
+theorem minus_minus: ∀n,m,p:nat. p ≤ m → m ≤ n →
+  p+(n-m) = n-(m-p).
+#n #m #p #lepm #lemn
+@sym_eq @plus_to_minus <associative_plus <plus_minus_m_m //
+<commutative_plus <plus_minus_m_m //
+qed.
+
 (*********************** boolean arithmetics ********************) 
 include "basics/bool.ma".
 
diff --git a/matita/matita/lib/arithmetics/primes.ma b/matita/matita/lib/arithmetics/primes.ma
index 2c4897d06..71e372f96 100644
--- a/matita/matita/lib/arithmetics/primes.ma
+++ b/matita/matita/lib/arithmetics/primes.ma
@@ -81,7 +81,7 @@ theorem eq_mod_to_divides: ∀n,m,q. O < q →
   |@(quotient ?? ((div n q)-(div m q)))
    >distributive_times_minus >commutative_times
    >(commutative_times q) cut((n/q)*q = n - (n \mod q)) [//] #H
-   >H >minus_minus >eqmod >commutative_plus 
+   >H >minus_plus >eqmod >commutative_plus 
    <div_mod //
   ]
 qed.
diff --git a/matita/matita/lib/arithmetics/sigma_pi.ma b/matita/matita/lib/arithmetics/sigma_pi.ma
new file mode 100644
index 000000000..d92d525b7
--- /dev/null
+++ b/matita/matita/lib/arithmetics/sigma_pi.ma
@@ -0,0 +1,747 @@
+(*
+    ||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/bigops.ma".
+
+definition natAop ≝ mk_Aop nat 0 plus (λa.refl ? a) (λn.sym_eq ??? (plus_n_O n)) 
+   (λa,b,c.sym_eq ??? (associative_plus a b c)).
+   
+definition natACop ≝ mk_ACop nat 0 natAop commutative_plus.
+
+definition natDop ≝ mk_Dop nat 0 natACop times (λn.(sym_eq ??? (times_n_O n))) 
+   distributive_times_plus.
+
+unification hint  0 ≔ ;
+   S ≟ natAop
+(* ---------------------------------------- *) ⊢ 
+   plus ≡ op ? ? S.
+
+unification hint  0 ≔ ;
+   S ≟ natACop
+(* ---------------------------------------- *) ⊢ 
+   plus ≡ op ? ? S.
+
+unification hint  0 ≔ ;
+   S ≟ natDop
+(* ---------------------------------------- *) ⊢ 
+   plus ≡ sum ? ? S.
+   
+unification hint  0 ≔ ;
+   S ≟ natDop
+(* ---------------------------------------- *) ⊢ 
+   times ≡ prod ? ? S.   
+   
+(* Sigma e Pi *)
+
+notation "∑_{ ident i < n | p } f"
+  with precedence 80
+for @{'bigop $n plus 0 (λ${ident i}.$p) (λ${ident i}. $f)}.
+
+notation "∑_{ ident i < n } f"
+  with precedence 80
+for @{'bigop $n plus 0 (λ${ident i}.true) (λ${ident i}. $f)}.
+
+notation "∑_{ ident j ∈ [a,b[ } f"
+  with precedence 80
+for @{'bigop ($b-$a) plus 0 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
+  (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
+  
+notation "∑_{ ident j ∈ [a,b[ | p } f"
+  with precedence 80
+for @{'bigop ($b-$a) plus 0 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
+  (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
+ 
+notation "∏_{ ident i < n | p} f"
+  with precedence 80
+for @{'bigop $n times 1 (λ${ident i}.$p) (λ${ident i}. $f)}.
+ 
+notation "∏_{ ident i < n } f"
+  with precedence 80
+for @{'bigop $n times 1 (λ${ident i}.true) (λ${ident i}. $f)}.
+
+notation "∏_{ ident j ∈ [a,b[ } f"
+  with precedence 80
+for @{'bigop ($b-$a) times 1 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
+  (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
+  
+notation "∏_{ ident j ∈ [a,b[ | p } f"
+  with precedence 80
+for @{'bigop ($b-$a) times 1 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
+  (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
+
+ 
+(*
+    
+definition p_ord_times \def
+\lambda p,m,x.
+  match p_ord x p with
+  [pair q r \Rightarrow r*m+q].
+  
+theorem  eq_p_ord_times: \forall p,m,x.
+p_ord_times p m x = (ord_rem x p)*m+(ord x p).
+intros.unfold p_ord_times. unfold ord_rem.
+unfold ord.
+elim (p_ord x p).
+reflexivity.
+qed.
+
+theorem div_p_ord_times: 
+\forall p,m,x. ord x p < m \to p_ord_times p m x / m = ord_rem x p.
+intros.rewrite > eq_p_ord_times.
+apply div_plus_times.
+assumption.
+qed.
+
+theorem mod_p_ord_times: 
+\forall p,m,x. ord x p < m \to p_ord_times p m x \mod m = ord x p.
+intros.rewrite > eq_p_ord_times.
+apply mod_plus_times.
+assumption.
+qed.
+
+lemma lt_times_to_lt_O: \forall i,n,m:nat. i < n*m \to O < m.
+intros.
+elim (le_to_or_lt_eq O ? (le_O_n m))
+  [assumption
+  |apply False_ind.
+   rewrite < H1 in H.
+   rewrite < times_n_O in H.
+   apply (not_le_Sn_O ? H)
+  ]
+qed.
+
+theorem iter_p_gen_knm:
+\forall A:Type.
+\forall baseA: A.
+\forall plusA: A \to A \to A. 
+(symmetric A plusA) \to 
+(associative A plusA) \to 
+(\forall a:A.(plusA a  baseA) = a)\to
+\forall g: nat \to A.
+\forall h2:nat \to nat \to nat.
+\forall h11,h12:nat \to nat. 
+\forall k,n,m.
+\forall p1,p21:nat \to bool.
+\forall p22:nat \to nat \to bool.
+(\forall x. x < k \to p1 x = true \to 
+p21 (h11 x) = true \land p22 (h11 x) (h12 x) = true
+\land h2 (h11 x) (h12 x) = x 
+\land (h11 x) < n \land (h12 x) < m) \to
+(\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to 
+p1 (h2 i j) = true \land 
+h11 (h2 i j) = i \land h12 (h2 i j) = j
+\land h2 i j < k) \to
+iter_p_gen k p1 A g baseA plusA =
+iter_p_gen n p21 A (\lambda x:nat.iter_p_gen m (p22 x) A (\lambda y. g (h2 x y)) baseA plusA) baseA plusA.
+intros.
+rewrite < (iter_p_gen2' n m p21 p22 ? ? ? ? H H1 H2).
+apply sym_eq.
+apply (eq_iter_p_gen_gh A baseA plusA H H1 H2 g ? (\lambda x.(h11 x)*m+(h12 x)))
+ [intros.
+  elim (H4 (i/m) (i \mod m));clear H4
+   [elim H7.clear H7.
+    elim H4.clear H4.
+    assumption
+   |apply (lt_times_to_lt_div ? ? ? H5)
+   |apply lt_mod_m_m.
+    apply (lt_times_to_lt_O ? ? ? H5)
+   |apply (andb_true_true ? ? H6)
+   |apply (andb_true_true_r ? ? H6)
+   ]
+ |intros.
+  elim (H4 (i/m) (i \mod m));clear H4
+   [elim H7.clear H7.
+    elim H4.clear H4.
+    rewrite > H10.
+    rewrite > H9.
+    apply sym_eq.
+    apply div_mod.
+    apply (lt_times_to_lt_O ? ? ? H5)
+   |apply (lt_times_to_lt_div ? ? ? H5)
+   |apply lt_mod_m_m.
+    apply (lt_times_to_lt_O ? ? ? H5)  
+   |apply (andb_true_true ? ? H6)
+   |apply (andb_true_true_r ? ? H6)
+   ]
+ |intros.
+  elim (H4 (i/m) (i \mod m));clear H4
+   [elim H7.clear H7.
+    elim H4.clear H4.
+    assumption
+   |apply (lt_times_to_lt_div ? ? ? H5)
+   |apply lt_mod_m_m.
+    apply (lt_times_to_lt_O ? ? ? H5)
+   |apply (andb_true_true ? ? H6)
+   |apply (andb_true_true_r ? ? H6)
+   ]
+ |intros.
+  elim (H3 j H5 H6).
+  elim H7.clear H7.
+  elim H9.clear H9.
+  elim H7.clear H7.
+  rewrite > div_plus_times
+   [rewrite > mod_plus_times
+     [rewrite > H9.
+      rewrite > H12.
+      reflexivity.
+     |assumption
+     ]
+   |assumption
+   ]
+ |intros.
+  elim (H3 j H5 H6).
+  elim H7.clear H7.
+  elim H9.clear H9.
+  elim H7.clear H7. 
+  rewrite > div_plus_times
+   [rewrite > mod_plus_times
+     [assumption
+     |assumption
+     ]
+   |assumption
+   ]
+ |intros.
+  elim (H3 j H5 H6).
+  elim H7.clear H7.
+  elim H9.clear H9.
+  elim H7.clear H7. 
+  apply (lt_to_le_to_lt ? ((h11 j)*m+m))
+   [apply monotonic_lt_plus_r.
+    assumption
+   |rewrite > sym_plus.
+    change with ((S (h11 j)*m) \le n*m).
+    apply monotonic_le_times_l.
+    assumption
+   ]
+ ]
+qed.
+
+theorem iter_p_gen_divides:
+\forall A:Type.
+\forall baseA: A.
+\forall plusA: A \to A \to A. 
+\forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to 
+\forall g: nat \to A.
+(symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a)
+
+\to
+
+iter_p_gen (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) A g baseA plusA =
+iter_p_gen (S n) (\lambda x.divides_b x n) A
+  (\lambda x.iter_p_gen (S m) (\lambda y.true) A (\lambda y.g (x*(exp p y))) baseA plusA) baseA plusA.
+intros.
+cut (O < p)
+  [rewrite < (iter_p_gen2 ? ? ? ? ? ? ? ? H3 H4 H5).
+   apply (trans_eq ? ? 
+    (iter_p_gen (S n*S m) (\lambda x:nat.divides_b (x/S m) n) A
+       (\lambda x:nat.g (x/S m*(p)\sup(x\mod S m)))  baseA plusA) )
+    [apply sym_eq.
+     apply (eq_iter_p_gen_gh ? ? ? ? ? ? g ? (p_ord_times p (S m)))
+      [ assumption
+      | assumption
+      | assumption
+      |intros.
+       lapply (divides_b_true_to_lt_O ? ? H H7).
+       apply divides_to_divides_b_true
+        [rewrite > (times_n_O O).
+         apply lt_times
+          [assumption
+          |apply lt_O_exp.assumption
+          ]
+        |apply divides_times
+          [apply divides_b_true_to_divides.assumption
+          |apply (witness ? ? (p \sup (m-i \mod (S m)))).
+           rewrite < exp_plus_times.
+           apply eq_f.
+           rewrite > sym_plus.
+           apply plus_minus_m_m.
+           autobatch by le_S_S_to_le, lt_mod_m_m, lt_O_S;
+          ]
+        ]
+      |intros.
+       lapply (divides_b_true_to_lt_O ? ? H H7).
+       unfold p_ord_times.
+       rewrite > (p_ord_exp1 p ? (i \mod (S m)) (i/S m))
+        [change with ((i/S m)*S m+i \mod S m=i).
+         apply sym_eq.
+         apply div_mod.
+         apply lt_O_S
+        |assumption
+        |unfold Not.intro.
+         apply H2.
+         apply (trans_divides ? (i/ S m))
+          [assumption|
+           apply divides_b_true_to_divides;assumption]
+        |apply sym_times.
+        ]
+      |intros.
+       apply le_S_S.
+       apply le_times
+        [apply le_S_S_to_le.
+         change with ((i/S m) < S n).
+         apply (lt_times_to_lt_l m).
+         apply (le_to_lt_to_lt ? i);[2:assumption]
+         autobatch by eq_plus_to_le, div_mod, lt_O_S.
+        |apply le_exp
+          [assumption
+          |apply le_S_S_to_le.
+           apply lt_mod_m_m.
+           apply lt_O_S
+          ]
+        ]
+      |intros.
+       cut (ord j p < S m)
+        [rewrite > div_p_ord_times
+          [apply divides_to_divides_b_true
+            [apply lt_O_ord_rem
+             [elim H1.assumption
+             |apply (divides_b_true_to_lt_O ? ? ? H7).
+               rewrite > (times_n_O O).
+               apply lt_times
+               [assumption|apply lt_O_exp.assumption]
+             ]
+           |cut (n = ord_rem (n*(exp p m)) p)
+              [rewrite > Hcut2.
+               apply divides_to_divides_ord_rem
+                [apply (divides_b_true_to_lt_O ? ? ? H7).
+                 rewrite > (times_n_O O).
+                 apply lt_times
+                 [assumption|apply lt_O_exp.assumption]
+                 |rewrite > (times_n_O O).
+                   apply lt_times
+                  [assumption|apply lt_O_exp.assumption]
+               |assumption
+               |apply divides_b_true_to_divides.
+                assumption
+               ]
+              |unfold ord_rem.
+              rewrite > (p_ord_exp1 p ? m n)
+                [reflexivity
+               |assumption
+                |assumption
+               |apply sym_times
+               ]
+             ]
+            ]
+          |assumption
+          ]
+        |cut (m = ord (n*(exp p m)) p)
+          [apply le_S_S.
+           rewrite > Hcut1.
+           apply divides_to_le_ord
+            [apply (divides_b_true_to_lt_O ? ? ? H7).
+             rewrite > (times_n_O O).
+             apply lt_times
+              [assumption|apply lt_O_exp.assumption]
+            |rewrite > (times_n_O O).
+             apply lt_times
+              [assumption|apply lt_O_exp.assumption]
+            |assumption
+            |apply divides_b_true_to_divides.
+             assumption
+            ]
+          |unfold ord.
+           rewrite > (p_ord_exp1 p ? m n)
+            [reflexivity
+            |assumption
+            |assumption
+            |apply sym_times
+            ]
+          ]
+        ]
+      |intros.
+       cut (ord j p < S m)
+        [rewrite > div_p_ord_times
+          [rewrite > mod_p_ord_times
+            [rewrite > sym_times.
+             apply sym_eq.
+             apply exp_ord
+              [elim H1.assumption
+              |apply (divides_b_true_to_lt_O ? ? ? H7).
+               rewrite > (times_n_O O).
+               apply lt_times
+                [assumption|apply lt_O_exp.assumption]
+              ]
+           |cut (m = ord (n*(exp p m)) p)
+             [apply le_S_S.
+              rewrite > Hcut2.
+              apply divides_to_le_ord
+               [apply (divides_b_true_to_lt_O ? ? ? H7).
+                rewrite > (times_n_O O).
+                apply lt_times
+                 [assumption|apply lt_O_exp.assumption]
+               |rewrite > (times_n_O O).
+                apply lt_times
+                 [assumption|apply lt_O_exp.assumption]
+               |assumption
+               |apply divides_b_true_to_divides.
+                assumption
+               ]
+             |unfold ord.
+              rewrite > (p_ord_exp1 p ? m n)
+                [reflexivity
+                |assumption
+                |assumption
+                |apply sym_times
+                ]
+              ]
+            ]
+          |assumption
+          ]
+        |cut (m = ord (n*(exp p m)) p)
+          [apply le_S_S.
+           rewrite > Hcut1.
+           apply divides_to_le_ord
+            [apply (divides_b_true_to_lt_O ? ? ? H7).
+             rewrite > (times_n_O O).
+             apply lt_times
+              [assumption|apply lt_O_exp.assumption]
+            |rewrite > (times_n_O O).
+             apply lt_times
+              [assumption|apply lt_O_exp.assumption]
+            |assumption
+            |apply divides_b_true_to_divides.
+             assumption
+            ]
+          |unfold ord.
+           rewrite > (p_ord_exp1 p ? m n)
+            [reflexivity
+            |assumption
+            |assumption
+            |apply sym_times
+            ]
+          ]
+        ]
+      |intros.
+       rewrite > eq_p_ord_times.
+       rewrite > sym_plus.
+       apply (lt_to_le_to_lt ? (S m +ord_rem j p*S m))
+        [apply lt_plus_l.
+         apply le_S_S.
+         cut (m = ord (n*(p \sup m)) p)
+          [rewrite > Hcut1.
+           apply divides_to_le_ord
+            [apply (divides_b_true_to_lt_O ? ? ? H7).
+             rewrite > (times_n_O O).
+             apply lt_times
+              [assumption|apply lt_O_exp.assumption]
+            |rewrite > (times_n_O O).
+             apply lt_times
+              [assumption|apply lt_O_exp.assumption]
+            |assumption
+            |apply divides_b_true_to_divides.
+             assumption
+            ]
+          |unfold ord.
+           rewrite > sym_times.
+           rewrite > (p_ord_exp1 p ? m n)
+            [reflexivity
+            |assumption
+            |assumption
+            |reflexivity
+            ]
+          ]
+        |change with (S (ord_rem j p)*S m \le S n*S m).
+         apply le_times_l.
+         apply le_S_S.
+         cut (n = ord_rem (n*(p \sup m)) p)
+          [rewrite > Hcut1.
+           apply divides_to_le
+            [apply lt_O_ord_rem
+              [elim H1.assumption
+              |rewrite > (times_n_O O).
+               apply lt_times
+                [assumption|apply lt_O_exp.assumption]
+              ]
+            |apply divides_to_divides_ord_rem
+              [apply (divides_b_true_to_lt_O ? ? ? H7).
+               rewrite > (times_n_O O).
+               apply lt_times
+                [assumption|apply lt_O_exp.assumption]
+              |rewrite > (times_n_O O).
+               apply lt_times
+                [assumption|apply lt_O_exp.assumption]
+              |assumption
+              |apply divides_b_true_to_divides.
+               assumption
+              ]
+            ]
+        |unfold ord_rem.
+         rewrite > sym_times.
+         rewrite > (p_ord_exp1 p ? m n)
+          [reflexivity
+          |assumption
+          |assumption
+          |reflexivity
+          ]
+        ]
+      ]
+    ]
+  |apply eq_iter_p_gen
+  
+    [intros.
+     elim (divides_b (x/S m) n);reflexivity
+    |intros.reflexivity
+    ]
+  ]
+|elim H1.apply lt_to_le.assumption
+]
+qed.
+    
+
+
+theorem iter_p_gen_2_eq: 
+\forall A:Type.
+\forall baseA: A.
+\forall plusA: A \to A \to A. 
+(symmetric A plusA) \to 
+(associative A plusA) \to 
+(\forall a:A.(plusA a  baseA) = a)\to
+\forall g: nat \to nat \to A.
+\forall h11,h12,h21,h22: nat \to nat \to nat. 
+\forall n1,m1,n2,m2.
+\forall p11,p21:nat \to bool.
+\forall p12,p22:nat \to nat \to bool.
+(\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to 
+p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
+\land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
+\land h11 i j < n1 \land h12 i j < m1) \to
+(\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to 
+p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
+\land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
+\land (h21 i j) < n2 \land (h22 i j) < m2) \to
+iter_p_gen n1 p11 A 
+     (\lambda x:nat .iter_p_gen m1 (p12 x) A (\lambda y. g x y) baseA plusA) 
+     baseA plusA =
+iter_p_gen n2 p21 A 
+    (\lambda x:nat .iter_p_gen m2 (p22 x) A  (\lambda y. g (h11 x y) (h12 x y)) baseA plusA )
+    baseA plusA.
+
+intros.
+rewrite < (iter_p_gen2' ? ? ? ? ? ? ? ? H H1 H2).
+letin ha:= (\lambda x,y.(((h11 x y)*m1) + (h12 x y))).
+letin ha12:= (\lambda x.(h21 (x/m1) (x \mod m1))).
+letin ha22:= (\lambda x.(h22 (x/m1) (x \mod m1))).
+
+apply (trans_eq ? ? 
+(iter_p_gen n2 p21 A (\lambda x:nat. iter_p_gen m2 (p22 x) A
+ (\lambda y:nat.(g (((h11 x y)*m1+(h12 x y))/m1) (((h11 x y)*m1+(h12 x y))\mod m1))) baseA plusA ) baseA plusA))
+[
+  apply (iter_p_gen_knm A baseA plusA H H1 H2 (\lambda e. (g (e/m1) (e \mod m1))) ha ha12 ha22);intros
+  [ elim (and_true ? ? H6).
+    cut(O \lt m1)
+    [ cut(x/m1 < n1)
+      [ cut((x \mod m1) < m1)
+        [ elim (H4 ? ? Hcut1 Hcut2 H7 H8).
+          elim H9.clear H9.
+          elim H11.clear H11.
+          elim H9.clear H9.
+          elim H11.clear H11.
+          split
+          [ split
+            [ split
+              [ split
+                [ assumption
+                | assumption
+                ]
+              | unfold ha.
+                unfold ha12.
+                unfold ha22.
+                rewrite > H14.
+                rewrite > H13.
+                apply sym_eq.
+                apply div_mod.
+                assumption
+              ]
+            | assumption
+            ]
+          | assumption
+          ]
+        | apply lt_mod_m_m.
+          assumption
+        ]
+      | apply (lt_times_n_to_lt m1)
+        [ assumption
+        | apply (le_to_lt_to_lt ? x)
+          [ apply (eq_plus_to_le ? ? (x \mod m1)).
+            apply div_mod.
+            assumption
+          | assumption
+        ]
+      ]  
+    ]
+    | apply not_le_to_lt.unfold.intro.
+      generalize in match H5.
+      apply (le_n_O_elim ? H9).
+      rewrite < times_n_O.
+      apply le_to_not_lt.
+      apply le_O_n.              
+    ]
+  | elim (H3 ? ? H5 H6 H7 H8).
+    elim H9.clear H9.
+    elim H11.clear H11.
+    elim H9.clear H9.
+    elim H11.clear H11.
+    cut(((h11 i j)*m1 + (h12 i j))/m1 = (h11 i j))
+    [ cut(((h11 i j)*m1 + (h12 i j)) \mod m1 = (h12 i j))
+      [ split
+        [ split
+          [ split
+            [ apply true_to_true_to_andb_true
+              [ rewrite > Hcut.
+                assumption
+              | rewrite > Hcut1.
+                rewrite > Hcut.
+                assumption
+              ] 
+            | unfold ha.
+              unfold ha12.
+              rewrite > Hcut1.
+              rewrite > Hcut.
+              assumption
+            ]
+          | unfold ha.
+            unfold ha22.
+            rewrite > Hcut1.
+            rewrite > Hcut.
+            assumption            
+          ]
+        | cut(O \lt m1)
+          [ cut(O \lt n1)      
+            [ apply (lt_to_le_to_lt ? ((h11 i j)*m1 + m1) )
+              [ unfold ha.
+                apply (lt_plus_r).
+                assumption
+              | rewrite > sym_plus.
+                rewrite > (sym_times (h11 i j) m1).
+                rewrite > times_n_Sm.
+                rewrite > sym_times.
+                apply (le_times_l).
+                assumption  
+              ]
+            | apply not_le_to_lt.unfold.intro.
+              generalize in match H12.
+              apply (le_n_O_elim ? H11).       
+              apply le_to_not_lt.
+              apply le_O_n
+            ]
+          | apply not_le_to_lt.unfold.intro.
+            generalize in match H10.
+            apply (le_n_O_elim ? H11).       
+            apply le_to_not_lt.
+            apply le_O_n
+          ]  
+        ]
+      | rewrite > (mod_plus_times m1 (h11 i j) (h12 i j)).
+        reflexivity.
+        assumption
+      ]     
+    | rewrite > (div_plus_times m1 (h11 i j) (h12 i j)).
+      reflexivity.
+      assumption
+    ]
+  ]
+| apply (eq_iter_p_gen1)
+  [ intros. reflexivity 
+  | intros.
+    apply (eq_iter_p_gen1)
+    [ intros. reflexivity
+    | intros.
+      rewrite > (div_plus_times)
+      [ rewrite > (mod_plus_times)
+        [ reflexivity
+        | elim (H3 x x1 H5 H7 H6 H8).
+          assumption
+        ]
+      | elim (H3 x x1 H5 H7 H6 H8).       
+        assumption
+      ]
+    ]
+  ]
+]
+qed.
+
+theorem iter_p_gen_iter_p_gen: 
+\forall A:Type.
+\forall baseA: A.
+\forall plusA: A \to A \to A. 
+(symmetric A plusA) \to 
+(associative A plusA) \to 
+(\forall a:A.(plusA a  baseA) = a)\to
+\forall g: nat \to nat \to A.
+\forall n,m.
+\forall p11,p21:nat \to bool.
+\forall p12,p22:nat \to nat \to bool.
+(\forall x,y. x < n \to y < m \to 
+ (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to
+iter_p_gen n p11 A 
+  (\lambda x:nat.iter_p_gen m (p12 x) A (\lambda y. g x y) baseA plusA) 
+  baseA plusA =
+iter_p_gen m p21 A 
+  (\lambda y:nat.iter_p_gen n (p22 y) A  (\lambda x. g x y) baseA plusA )
+  baseA plusA.
+intros.
+apply (iter_p_gen_2_eq A baseA plusA H H1 H2 (\lambda x,y. g x y) (\lambda x,y.y) (\lambda x,y.x) (\lambda x,y.y) (\lambda x,y.x)
+       n m m n p11 p21 p12 p22)
+  [intros.split
+    [split
+      [split
+        [split
+          [split
+            [apply (andb_true_true ? (p12 j i)).
+             rewrite > H3
+              [rewrite > H6.rewrite > H7.reflexivity
+              |assumption
+              |assumption
+              ]
+            |apply (andb_true_true_r (p11 j)).
+             rewrite > H3
+              [rewrite > H6.rewrite > H7.reflexivity
+              |assumption
+              |assumption
+              ]
+            ]
+          |reflexivity
+          ]
+        |reflexivity
+        ]
+      |assumption
+      ]
+    |assumption
+    ]
+  |intros.split
+    [split
+      [split
+        [split
+          [split
+            [apply (andb_true_true ? (p22 j i)).
+             rewrite < H3
+              [rewrite > H6.rewrite > H7.reflexivity
+              |assumption
+              |assumption
+              ]
+            |apply (andb_true_true_r (p21 j)).
+             rewrite < H3
+              [rewrite > H6.rewrite > H7.reflexivity
+              |assumption
+              |assumption
+              ]
+            ]
+          |reflexivity
+          ]
+        |reflexivity
+        ]
+      |assumption
+      ]
+    |assumption
+    ]
+  ]
+qed. *)
\ No newline at end of file