X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fbigops.ma;h=e51cd799aa11533605db577807b5165ffdd6aff5;hb=fd12cbee622c58bc45089d62c3e6f131c238beb5;hp=1bd7c1613f0bea792f5dd91f80a23d88476e833e;hpb=16a95f57b09ae92ea24ab2addd02c1d0be80f109;p=helm.git

diff --git a/matita/matita/lib/arithmetics/bigops.ma b/matita/matita/lib/arithmetics/bigops.ma
index 1bd7c1613..e51cd799a 100644
--- a/matita/matita/lib/arithmetics/bigops.ma
+++ b/matita/matita/lib/arithmetics/bigops.ma
@@ -9,1688 +9,417 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "arithmetics/nat.ma".
+include "basics/types.ma".
+include "arithmetics/div_and_mod.ma".
 
-let rec bigop' (n:nat) (filter: nat → bool) (A:Type[0]) (f: nat → A) 
-   (nil: A) (op: A → A → A)  ≝
-  match n with
-   [ O ⇒ nil
-   | S k ⇒ 
-      match filter k with
-      [true ⇒ op (f k) (bigop' k filter A f nil op)
-      |false ⇒ bigop' k filter A f nil op]
-   ].
+definition sameF_upto: nat → ∀A.relation(nat→A)  ≝
+λk.λA.λf,g.∀i. i < k → f i = g i.
+     
+definition sameF_p: nat → (nat → bool) →∀A.relation(nat→A)  ≝
+λk,p,A,f,g.∀i. i < k → p i = true → f i = g i.
 
-record range (A:Type[0]): Type[0] ≝
-  {h:nat→A; upto:nat; filter:nat→bool}.
+lemma sameF_upto_le: ∀A,f,g,n,m. 
+ n ≤m → sameF_upto m A f g → sameF_upto n A f g.
+#A #f #g #n #m #lenm #samef #i #ltin @samef /2 by lt_to_le_to_lt/
+qed.
 
-definition same_upto: nat → ∀A.relation (range A) ≝
-λk.λA.λI,J.
-  ∀i. i < k → 
-    ((filter A I i) = (filter A J i) ∧
-     ((filter A I i) = true → (h A I i) = (h A J i))).
-     
-definition same: ∀A.relation (range A) ≝
-λA.λI,J. (upto A I = upto A J) ∧ same_upto (upto A I) A I J.
+lemma sameF_p_le: ∀A,p,f,g,n,m. 
+ n ≤m → sameF_p m p A f g → sameF_p n p A f g.
+#A #p #f #g #n #m #lenm #samef #i #ltin #pi @samef /2 by lt_to_le_to_lt/
+qed.
 
-definition pad: ∀A.nat→range A→range A ≝
-  λA.λk.λI.mk_range A (h A I) k 
-   (λi.if_then_else ? (leb (upto A I) i) false (filter A I i)).
-  
-definition same1: ∀A.relation (range A) ≝
-λA.λI,J.
-  let maxIJ ≝ (max (upto A I) (upto A J)) in
-  same_upto maxIJ A (pad A maxIJ I) (pad A maxIJ J).
+(*
+definition sumF ≝ λA.λf,g:nat → A.λn,i.
+if_then_else ? (leb n i) (g (i-n)) (f i). 
 
-(*     
-definition same: ∀A.relation (range A) ≝
-λA.λI,J.
-  ∀i. i < max (upto A I) (upto A J) → 
-    ((filter A I i) = (filter A J i) ∧
-     ((filter A I i) = true → (h A I i) = (h A J i))). *)
-     
-definition bigop: ∀A,B:Type[0].(range A)→B→(B→B→B)→(A→B)→B ≝
-  λA,B.λI.λnil.λop.λf. 
-    bigop' (upto A I) (filter A I) B (λx.f(h A I x)) nil op.
+lemma sumF_unfold: ∀A,f,g,n,i. 
+sumF A f g n i = if_then_else ? (leb n i) (g (i-n)) (f i). 
+// qed. *)
 
-theorem same_bigop: ∀A,B.∀I,J:range A. ∀nil.∀op.∀f.
-  same A I J → bigop A B I nil op f = bigop A B J nil op f. 
-#A #B #I #J #nil #op #f * #equp normalize <equp #same
-@(le_gen ? (upto A I)) #i (elim i) // #i #Hind #lti
-(lapply (same i lti)) * #eqfilter 
-(lapply (Hind (transitive_le … (le_n_Sn i) (lti)))) #eqbigop
-normalize <eqfilter (cases (filter A I i)) normalize //
-#H (lapply (H (refl ??))) // qed.
+definition prodF ≝
+ λA,B.λf:nat→A.λg:nat→B.λm,x.〈 f(div x m), g(mod x m) 〉.
 
-theorem pad_bigog: ∀A,B.∀I:range A. ∀nil.∀op.∀f.∀k.
-  upto A I ≤ k → bigop A B I nil op f = bigop A B (pad A k I) nil op f. 
-#A #B #I #nil #op #f #k #lek (elim lek) 
-[@same_bigop % // #i #lti % // normalize 
- >(not_le_to_leb_false …) // @lt_to_not_le //
-|#n #leup #Hind normalize <Hind >(le_to_leb_true … leup) normalize //
-] qed.
+(* bigop *)
+let rec bigop (n:nat) (p:nat → bool) (B:Type[0])
+   (nil: B) (op: B → B → B)  (f: nat → B) ≝
+  match n with
+   [ O ⇒ nil
+   | S k ⇒ 
+      match p k with
+      [true ⇒ op (f k) (bigop k p B nil op f)
+      |false ⇒ bigop k p B nil op f]
+   ].
+   
+notation "\big  [ op , nil ]_{ ident i < n | p } f"
+  with precedence 80
+for @{'bigop $n $op $nil (λ${ident i}. $p) (λ${ident i}. $f)}.
 
-theorem iter_p_gen_false: \forall A:Type. \forall g: nat \to A. \forall baseA:A.
-\forall plusA: A \to A \to A. \forall n.
-iter_p_gen n (\lambda x.false) A g baseA plusA = baseA.
-intros.
-elim n
-[ reflexivity
-| simplify.
-  assumption
-]
-qed.
+notation "\big [ op , nil ]_{ ident i < n } f"
+  with precedence 80
+for @{'bigop $n $op $nil (λ${ident i}.true) (λ${ident i}. $f)}.
 
-theorem iter_p_gen_plusA: \forall A:Type. \forall n,k:nat.\forall p:nat \to bool.
-\forall g: nat \to A. \forall baseA:A. \forall plusA: A \to A \to A.
-(symmetric A plusA) \to (\forall a:A. (plusA a baseA) = a) \to (associative A plusA)
-\to
-iter_p_gen (k + n) p A g baseA plusA 
-= (plusA (iter_p_gen k (\lambda x.p (x+n)) A (\lambda x.g (x+n)) baseA plusA)
-         (iter_p_gen n p A g baseA plusA)).
-intros.
+interpretation "bigop" 'bigop n op nil p f = (bigop n p ? nil op f).
 
-elim k
-[ simplify.
-  rewrite > H in \vdash (? ? ? %).
-  rewrite > (H1 ?).
-  reflexivity
-| apply (bool_elim ? (p (n1+n)))
-  [ intro.     
-    rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
-    rewrite > (true_to_iter_p_gen_Sn n1 (\lambda x.p (x+n)) ? ? ? ? H4).
-    rewrite > (H2 (g (n1 + n)) ? ?).
-    rewrite < H3.
-    reflexivity
-  | intro.
-    rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
-    rewrite > (false_to_iter_p_gen_Sn n1 (\lambda x.p (x+n)) ? ? ? ? H4).
-    assumption
-  ]
-]
+notation "\big  [ op , nil ]_{ ident j ∈ [a,b[ | p } f"
+  with precedence 80
+for @{'bigop ($b-$a) $op $nil (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
+  (λ${ident j}.((λ${ident j}.$f)(${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)))
+  (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.  
+ 
+(* notation "\big  [ op , nil ]_{( term 55) a ≤ ident j < b | p } f"
+  with precedence 80
+for @{\big[$op,$nil]_{${ident j} < ($b-$a) | ((λ${ident j}.$p) (${ident j}+$a))}((λ${ident j}.$f)(${ident j}+$a))}.
+*)
+ 
+interpretation "bigop" 'bigop n op nil p f = (bigop n p ? nil op f).
+   
+lemma bigop_Strue: ∀k,p,B,nil,op.∀f:nat→B. p k = true →
+  \big[op,nil]_{i < S k | p i}(f i) =
+    op (f k) (\big[op,nil]_{i < k | p i}(f i)).
+#k #p #B #nil #op #f #H normalize >H // qed.
+
+lemma bigop_Sfalse: ∀k,p,B,nil,op.∀f:nat→B. p k = false →
+  \big[op,nil]_{ i < S k | p i}(f i) =
+    \big[op,nil]_{i < k | p i}(f i).
+#k #p #B #nil #op #f #H normalize >H // qed. 
+ 
+lemma same_bigop : ∀k,p1,p2,B,nil,op.∀f,g:nat→B. 
+  sameF_upto k bool p1 p2 → sameF_p k p1 B f g →
+  \big[op,nil]_{i < k | p1 i}(f i) = 
+    \big[op,nil]_{i < k | p2 i}(g i).
+#k #p1 #p2 #B #nil #op #f #g (elim k) // 
+#n #Hind #samep #samef normalize >Hind /2/
+<(samep … (le_n …)) cases(true_or_false (p1 n)) #H1 >H1 
+normalize // <(samef … (le_n …) H1) // 
 qed.
 
-theorem false_to_eq_iter_p_gen: \forall A:Type. \forall n,m:nat.\forall p:nat \to bool.
-\forall g: nat \to A. \forall baseA:A. \forall plusA: A \to A \to A. 
-n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false)
-\to iter_p_gen m p A g baseA plusA = iter_p_gen n p A g baseA plusA.
-intros 8.
-elim H
-[ reflexivity
-| simplify.
-  rewrite > H3
-  [ simplify.
-    apply H2.
-    intros.
-    apply H3
-    [ apply H4
-    | apply le_S.
-      assumption
-    ]
-  | assumption
-  |apply le_n
-  ]
-]
+theorem pad_bigop: ∀k,n,p,B,nil,op.∀f:nat→B. n ≤ k → 
+\big[op,nil]_{i < n | p i}(f i)
+  = \big[op,nil]_{i < k | if leb n i then false else p i}(f i).
+#k #n #p #B #nil #op #f #lenk (elim lenk) 
+  [@same_bigop #i #lti // >(not_le_to_leb_false …) /2/
+  |#j #leup #Hind >bigop_Sfalse >(le_to_leb_true … leup) // 
+  ] qed.
+  
+theorem pad_bigop1: ∀k,n,p,B,nil,op.∀f:nat→B. n ≤ k → 
+  (∀i. n ≤ i → i < k → p i = false) →
+  \big[op,nil]_{i < n | p i}(f i) 
+    = \big[op,nil]_{i < k | p i}(f i).
+#k #n #p #B #nil #op #f #lenk (elim lenk) 
+  [#_ @same_bigop #i #lti // 
+  |#j #leup #Hind #Hfalse >bigop_Sfalse 
+    [@Hind #i #leni #ltij @Hfalse // @le_S //  
+    |@Hfalse // 
+    ] 
+  ] 
 qed.
-
-(* a therem slightly more general than the previous one *)
-theorem or_false_eq_baseA_to_eq_iter_p_gen: \forall A:Type. \forall n,m:nat.\forall p:nat \to bool.
-\forall g: nat \to A. \forall baseA:A. \forall plusA: A \to A \to A.
-(\forall a. plusA baseA a = a) \to
-n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false \lor g i = baseA)
-\to iter_p_gen m p A g baseA plusA = iter_p_gen n p A g baseA plusA.
-intros 9.
-elim H1
-[reflexivity
-|apply (bool_elim ? (p n1));intro
-  [elim (H4 n1)
-    [apply False_ind.
-     apply not_eq_true_false.
-     rewrite < H5.
-     rewrite < H6.
-     reflexivity
-    |rewrite > true_to_iter_p_gen_Sn
-      [rewrite > H6.
-       rewrite > H.
-       apply H3.intros.
-       apply H4
-        [assumption
-        |apply le_S.assumption
-        ]
-      |assumption
-      ]
-    |assumption
-    |apply le_n
-    ]
-  |rewrite > false_to_iter_p_gen_Sn
-    [apply H3.intros.
-     apply H4
-      [assumption
-      |apply le_S.assumption
-      ]
-    |assumption
-    ]
-  ]
-]
+  
+theorem bigop_false: ∀n,B,nil,op.∀f:nat→B.
+  \big[op,nil]_{i < n | false }(f i) = nil.  
+#n #B #nil #op #f elim n // #n1 #Hind 
+>bigop_Sfalse // 
 qed.
-    
-theorem iter_p_gen2 : 
-\forall n,m:nat.
-\forall p1,p2:nat \to bool.
-\forall A:Type.
-\forall g: nat \to nat \to A.
-\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
-iter_p_gen (n*m) 
-  (\lambda x.andb (p1 (div x m)) (p2 (mod x m)))
-  A 
-  (\lambda x.g (div x m) (mod x m)) 
-  baseA
-  plusA  =
-iter_p_gen n p1 A
-  (\lambda x.iter_p_gen m p2 A (g x) baseA plusA)
-  baseA plusA.
-intros.
-elim n
-[ simplify.
-  reflexivity
-| apply (bool_elim ? (p1 n1))
-  [ intro.
-    rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
-    simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
-    rewrite > iter_p_gen_plusA
-    [ rewrite < H3.
-      apply eq_f2
-      [ apply eq_iter_p_gen
-        [ intros.
-          rewrite > sym_plus.
-          rewrite > (div_plus_times ? ? ? H5).
-          rewrite > (mod_plus_times ? ? ? H5).
-          rewrite > H4.
-          simplify.
-          reflexivity
-        | intros.
-          rewrite > sym_plus.
-          rewrite > (div_plus_times ? ? ? H5).
-          rewrite > (mod_plus_times ? ? ? H5).
-          reflexivity.   
-        ]
-      | reflexivity
-      ]
-    | assumption
-    | assumption
-    | assumption
-    ]
-  | intro.
-    rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
-    simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
-    rewrite > iter_p_gen_plusA
-    [ rewrite > H3.
-      apply (trans_eq ? ? (plusA baseA
-           (iter_p_gen n1 p1 A (\lambda x:nat.iter_p_gen m p2 A (g x) baseA plusA) baseA plusA )))
-      [ apply eq_f2
-        [ rewrite > (eq_iter_p_gen ? (\lambda x.false) A ? (\lambda x:nat.g ((x+n1*m)/m) ((x+n1*m)\mod m)))
-          [ apply iter_p_gen_false
-          | intros.
-            rewrite > sym_plus.
-            rewrite > (div_plus_times ? ? ? H5).
-            rewrite > (mod_plus_times ? ? ? H5).
-            rewrite > H4.
-            simplify.reflexivity
-          | intros.reflexivity.
-          ]
-        | reflexivity
-        ]
-      | rewrite < H.
-        rewrite > H2.
-        reflexivity.  
-      ]
-    | assumption
-    | assumption
-    | assumption
-    ]
+
+record Aop (A:Type[0]) (nil:A) : Type[0] ≝
+  {op :2> A → A → A; 
+   nill:∀a. op nil a = a; 
+   nilr:∀a. op a nil = a;
+   assoc: ∀a,b,c.op a (op b c) = op (op a b) c
+  }.
+  
+theorem pad_bigop_nil: ∀k,n,p,B,nil.∀op:Aop B nil.∀f:nat→B. n ≤ k → 
+  (∀i. n ≤ i → i < k → p i = false ∨ f i = nil) →
+  \big[op,nil]_{i < n | p i}(f i) 
+    = \big[op,nil]_{i < k | p i}(f i).
+#k #n #p #B #nil #op #f #lenk (elim lenk) 
+  [#_ @same_bigop #i #lti // 
+  |#j #leup #Hind #Hfalse cases (true_or_false (p j)) #Hpj
+    [>bigop_Strue // 
+     cut (f j = nil) 
+      [cases (Hfalse j leup (le_n … )) // >Hpj #H destruct (H)] #Hfj
+     >Hfj >nill @Hind #i #leni #ltij
+     cases (Hfalse i leni (le_S … ltij)) /2/
+    |>bigop_Sfalse // @Hind #i #leni #ltij
+     cases (Hfalse i leni (le_S … ltij)) /2/
+    ]  
   ]
-]
 qed.
 
-theorem iter_p_gen2': 
-\forall n,m:nat.
-\forall p1: nat \to bool.
-\forall p2: nat \to nat \to bool.
-\forall A:Type.
-\forall g: nat \to nat \to A.
-\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
-iter_p_gen (n*m) 
-  (\lambda x.andb (p1 (div x m)) (p2 (div x m)(mod x m)))
-  A 
-  (\lambda x.g (div x m) (mod x m)) 
-  baseA
-  plusA  =
-iter_p_gen n p1 A
-  (\lambda x.iter_p_gen m (p2 x) A (g x) baseA plusA)
-  baseA plusA.
-intros.
-elim n
-[ simplify.
-  reflexivity
-| apply (bool_elim ? (p1 n1))
-  [ intro.
-    rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
-    simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
-    rewrite > iter_p_gen_plusA
-    [ rewrite < H3.
-      apply eq_f2
-      [ apply eq_iter_p_gen
-        [ intros.
-          rewrite > sym_plus.
-          rewrite > (div_plus_times ? ? ? H5).
-          rewrite > (mod_plus_times ? ? ? H5).
-          rewrite > H4.
-          simplify.
-          reflexivity
-        | intros.
-          rewrite > sym_plus.
-          rewrite > (div_plus_times ? ? ? H5).
-          rewrite > (mod_plus_times ? ? ? H5).
-          reflexivity.   
-        ]
-      | reflexivity
-      ]
-    | assumption
-    | assumption
-    | assumption
-    ]
-  | intro.
-    rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
-    simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
-    rewrite > iter_p_gen_plusA
-    [ rewrite > H3.
-      apply (trans_eq ? ? (plusA baseA
-           (iter_p_gen n1 p1 A (\lambda x:nat.iter_p_gen m (p2 x) A (g x) baseA plusA) baseA plusA )))
-      [ apply eq_f2
-        [ rewrite > (eq_iter_p_gen ? (\lambda x.false) A ? (\lambda x:nat.g ((x+n1*m)/m) ((x+n1*m)\mod m)))
-          [ apply iter_p_gen_false
-          | intros.
-            rewrite > sym_plus.
-            rewrite > (div_plus_times ? ? ? H5).
-            rewrite > (mod_plus_times ? ? ? H5).
-            rewrite > H4.
-            simplify.reflexivity
-          | intros.reflexivity.
-          ]
-        | reflexivity
-        ]
-      | rewrite < H.
-        rewrite > H2.
-        reflexivity.  
-      ]
-    | assumption
-    | assumption
-    | assumption
-    ]
+theorem bigop_sum: ∀k1,k2,p1,p2,B.∀nil.∀op:Aop B nil.∀f,g:nat→B.
+op (\big[op,nil]_{i<k1|p1 i}(f i)) \big[op,nil]_{i<k2|p2 i}(g i) =
+      \big[op,nil]_{i<k1+k2|if leb k2 i then p1 (i-k2) else p2 i}
+        (if leb k2 i then f (i-k2) else g i).
+#k1 #k2 #p1 #p2 #B #nil #op #f #g (elim k1)
+  [normalize >nill @same_bigop #i #lti 
+   >(lt_to_leb_false … lti) normalize /2/
+  |#i #Hind normalize <minus_plus_m_m (cases (p1 i)) 
+   >(le_to_leb_true … (le_plus_n …)) normalize <Hind //
+   <assoc //
   ]
-]
 qed.
 
-lemma iter_p_gen_gi: 
-\forall A:Type.
-\forall g: nat \to A.
-\forall baseA:A.
-\forall plusA: A \to A \to A.
-\forall n,i:nat.
-\forall p:nat \to bool.
-(symmetric A plusA) \to  (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a) 
-  \to 
-  
-i < n \to p i = true \to
-(iter_p_gen n p A g baseA plusA) = 
-(plusA (g i) (iter_p_gen n (\lambda x:nat. andb (p x) (notb (eqb x i))) A g baseA plusA)).
-intros 5.
-elim n
-[ apply False_ind.
-  apply (not_le_Sn_O i).
-  assumption
-| apply (bool_elim ? (p n1));intro
-  [ elim (le_to_or_lt_eq i n1)
-    [ rewrite > true_to_iter_p_gen_Sn
-      [ rewrite > true_to_iter_p_gen_Sn
-        [ rewrite < (H2 (g i) ? ?).
-          rewrite > (H1 (g i) (g n1)).
-          rewrite > (H2 (g n1) ? ?).
-          apply eq_f2
-          [ reflexivity
-          | apply H
-            [ assumption
-            | assumption
-            | assumption 
-            | assumption
-            | assumption
-            ]
-          ]
-        | rewrite > H6.simplify.
-          change with (notb (eqb n1 i) = notb false).
-          apply eq_f.
-          apply not_eq_to_eqb_false.
-          unfold Not.intro.
-          apply (lt_to_not_eq ? ? H7).
-          apply sym_eq.assumption
-        ]
-      | assumption
-      ]
-    | rewrite > true_to_iter_p_gen_Sn
-      [ rewrite > H7.
-        apply eq_f2
-        [ reflexivity
-        | rewrite > false_to_iter_p_gen_Sn
-          [ apply eq_iter_p_gen
-            [ intros.
-              elim (p x)
-              [ simplify.
-                change with (notb false = notb (eqb x n1)).
-                apply eq_f.
-                apply sym_eq. 
-                apply not_eq_to_eqb_false.
-                apply (lt_to_not_eq ? ? H8)
-              | reflexivity
-              ]
-            | intros.
-              reflexivity
-            ]
-          | rewrite > H6.
-            rewrite > (eq_to_eqb_true ? ? (refl_eq ? n1)).
-            reflexivity
-          ]
-        ]
-      | assumption
-      ]
-    | apply le_S_S_to_le.
-      assumption
-    ]
-  | rewrite > false_to_iter_p_gen_Sn
-    [ elim (le_to_or_lt_eq i n1)
-      [ rewrite > false_to_iter_p_gen_Sn
-        [ apply H
-          [ assumption
-          | assumption
-          | assumption
-          | assumption
-          | assumption
-          ]
-        | rewrite > H6.reflexivity
-        ]
-      | apply False_ind. 
-        apply not_eq_true_false.
-        rewrite < H5.
-        rewrite > H7.
-        assumption
-      | apply le_S_S_to_le.
-        assumption
-      ]
-    | assumption
-    ]
-  ] 
-] 
+lemma plus_minus1: ∀a,b,c. c ≤ b → a + (b -c) = a + b -c.
+#a #b #c #lecb @sym_eq @plus_to_minus >(commutative_plus c) 
+>associative_plus <plus_minus_m_m //
 qed.
 
-(* invariance under permutation; single sum *)
-theorem eq_iter_p_gen_gh: 
-\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 h,h1: nat \to nat.
-\forall n,n1:nat.
-\forall p1,p2:nat \to bool.
-(\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to
-(\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to 
-(\forall i. i < n \to p1 i = true \to h i < n1) \to 
-(\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
-(\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to 
-(\forall j. j < n1 \to p2 j = true \to h1 j < n) \to 
-
-iter_p_gen n p1 A (\lambda x.g(h x)) baseA plusA = 
-iter_p_gen n1 p2 A g baseA plusA.
-intros 10.
-elim n
-[ generalize in match H8.
-  elim n1
-  [ reflexivity
-  | apply (bool_elim ? (p2 n2));intro
-    [ apply False_ind.
-      apply (not_le_Sn_O (h1 n2)).
-      apply H10
-      [ apply le_n
-      | assumption
-      ]
-    | rewrite > false_to_iter_p_gen_Sn
-      [ apply H9.
-        intros.  
-        apply H10
-        [ apply le_S.
-          apply H12
-        | assumption
-        ]
-      | assumption
-      ]
-    ]
-  ]
-| apply (bool_elim ? (p1 n1));intro
-  [ rewrite > true_to_iter_p_gen_Sn
-    [ rewrite > (iter_p_gen_gi A g baseA plusA n2 (h n1))
-      [ apply eq_f2
-        [ reflexivity
-        | apply H3
-          [ intros.
-            rewrite > H4
-            [ simplify.
-              change with ((\not eqb (h i) (h n1))= \not false).
-              apply eq_f.
-              apply not_eq_to_eqb_false.
-              unfold Not.
-              intro.
-              apply (lt_to_not_eq ? ? H11).
-              rewrite < H5
-              [ rewrite < (H5 n1)
-                [ apply eq_f.
-                  assumption
-                | apply le_n
-                | assumption
-                ]
-              | apply le_S.
-                assumption
-              | assumption
-              ]
-            | apply le_S.assumption
-            | assumption
-            ]
-          | intros.
-            apply H5
-            [ apply le_S.
-              assumption
-            | assumption
-            ]
-          | intros.
-            apply H6
-            [ apply le_S.assumption
-            | assumption
-            ]
-          | intros.
-            apply H7
-            [ assumption
-            | generalize in match H12.
-              elim (p2 j)
-              [ reflexivity
-              | assumption
-              ]
-            ]
-          | intros.
-            apply H8
-            [ assumption
-            | generalize in match H12.
-              elim (p2 j)
-              [ reflexivity
-              | assumption
-              ]
-            ]
-          | intros.
-            elim (le_to_or_lt_eq (h1 j) n1)
-            [ assumption
-            | generalize in match H12.
-              elim (p2 j)
-              [ simplify in H13.
-                absurd (j = (h n1))
-                [ rewrite < H13.
-                  rewrite > H8
-                  [ reflexivity
-                  | assumption
-                  | apply andb_true_true; [2: apply H12]
-                  ]
-                | apply eqb_false_to_not_eq.
-                  generalize in match H14.
-                  elim (eqb j (h n1))
-                  [ apply sym_eq.assumption
-                  | reflexivity
-                  ]
-                ]
-              | simplify in H14.
-                apply False_ind.
-                apply not_eq_true_false.
-                apply sym_eq.assumption
-              ]
-            | apply le_S_S_to_le.
-              apply H9
-              [ assumption
-              | generalize in match H12.
-                elim (p2 j)
-                [ reflexivity
-                | assumption
-                ]
-              ]
-            ]
-          ]
-        ]
-      | assumption  
-      | assumption
-      | assumption  
-      | apply H6
-        [ apply le_n
-        | assumption
-        ]
-      | apply H4
-        [ apply le_n
-        | assumption
-        ]
-      ]
-    | assumption
-    ]
-  | rewrite > false_to_iter_p_gen_Sn
-    [ apply H3
-      [ intros.
-        apply H4[apply le_S.assumption|assumption]
-      | intros.
-        apply H5[apply le_S.assumption|assumption]
-      | intros.
-        apply H6[apply le_S.assumption|assumption]
-      | intros.
-        apply H7[assumption|assumption]
-      | intros.
-        apply H8[assumption|assumption]
-      | intros.
-        elim (le_to_or_lt_eq (h1 j) n1)
-        [ assumption
-        | absurd (j = (h n1))
-          [ rewrite < H13.
-            rewrite > H8
-            [ reflexivity
-            | assumption
-            | assumption
-            ]
-          | unfold Not.intro.
-            apply not_eq_true_false.
-            rewrite < H10.
-            rewrite < H13.
-            rewrite > H7
-            [ reflexivity
-            | assumption
-            | assumption
-            ]
-          ]
-        | apply le_S_S_to_le.
-          apply H9
-          [ assumption
-          | assumption
-          ]
-        ]
-      ]
-    | assumption
-    ]
-  ]
-]
+theorem bigop_I: ∀n,p,B.∀nil.∀op:Aop B nil.∀f:nat→B.
+\big[op,nil]_{i∈[0,n[ |p i}(f i) = \big[op,nil]_{i < n|p i}(f i). 
+#n #p #B #nil #op #f <minus_n_O @same_bigop //
 qed.
-
-theorem eq_iter_p_gen_pred: 
-\forall A:Type.
-\forall baseA: A.
-\forall plusA: A \to A \to A.
-\forall n,p,g.
-p O = true \to
-(symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a) \to
-iter_p_gen (S n) (\lambda i.p (pred i)) A (\lambda i.g(pred i)) baseA plusA = 
-plusA (iter_p_gen n p A g baseA plusA) (g O).
-intros.
-elim n
-  [rewrite > true_to_iter_p_gen_Sn
-    [simplify.apply H1
-    |assumption
-    ]
-  |apply (bool_elim ? (p n1));intro
-    [rewrite > true_to_iter_p_gen_Sn
-      [rewrite > true_to_iter_p_gen_Sn in ⊢ (? ? ? %)
-        [rewrite > H2 in ⊢ (? ? ? %).
-         apply eq_f.assumption
-        |assumption
-        ]
-      |assumption
-      ]
-    |rewrite > false_to_iter_p_gen_Sn
-      [rewrite > false_to_iter_p_gen_Sn in ⊢ (? ? ? %);assumption
-      |assumption
+     
+theorem bigop_I_gen: ∀a,b,p,B.∀nil.∀op:Aop B nil.∀f:nat→B. a ≤b →
+\big[op,nil]_{i∈[a,b[ |p i}(f i) = \big[op,nil]_{i < b|leb a i ∧ p i}(f i). 
+#a #b elim b // -b #b #Hind #p #B #nil #op #f #lea
+cut (∀a,b. a ≤ b → S b - a = S (b -a)) 
+  [#a #b cases a // #a1 #lta1 normalize >eq_minus_S_pred >S_pred 
+   /2 by lt_plus_to_minus_r/] #Hcut
+cases (le_to_or_lt_eq … lea) #Ha
+  [cases (true_or_false (p b)) #Hcase
+    [>bigop_Strue [2: >Hcase >(le_to_leb_true a b) // @le_S_S_to_le @Ha]
+     >(Hcut … (le_S_S_to_le … Ha))
+     >bigop_Strue 
+      [@eq_f2 
+        [@eq_f <plus_minus_m_m [//|@le_S_S_to_le //] @Hind 
+        |@Hind @le_S_S_to_le //
+        ]
+      |<plus_minus_m_m // @le_S_S_to_le //
       ]
+   |>bigop_Sfalse [2: >Hcase cases (leb a b)//]
+     >(Hcut … (le_S_S_to_le … Ha)) >bigop_Sfalse
+      [@Hind @le_S_S_to_le // | <plus_minus_m_m // @le_S_S_to_le //]
     ]
+  |<Ha <minus_n_n whd in ⊢ (??%?); <(bigop_false a B nil op f) in ⊢ (??%?);
+   @same_bigop // #i #ltia >(not_le_to_leb_false a i) // @lt_to_not_le //
   ]
+qed.    
+     
+theorem bigop_sumI: ∀a,b,c,p,B.∀nil.∀op:Aop B nil.∀f:nat→B.
+a ≤ b → b ≤ c →
+\big[op,nil]_{i∈[a,c[ |p i}(f i) = 
+  op (\big[op,nil]_{i ∈ [b,c[ |p i}(f i)) 
+      \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_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.
-    
-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.
+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 (i/k2)) (p2 (i/k2) (i \mod k2))}
+     (f (i/k2) (i \mod k2)).
+#k1 #k2 #p1 #p2 #B #nil #op #f (elim k1) //
+#n #Hind cases(true_or_false (p1 n)) #Hp1
+  [>bigop_Strue // >Hind >bigop_sum @same_bigop
+   #i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2 by plus_minus/
+   #eqi [|#H] >eqi in ⊢ (???%);
+     >div_plus_times /2 by monotonic_lt_minus_l/ 
+     >Hp1 >(mod_plus_times …) /2 by refl, monotonic_lt_minus_l, eq_f/
+  |>bigop_Sfalse // >Hind >(pad_bigop (S n*k2)) // @same_bigop
+   #i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2 by plus_minus/
+   #eqi >eqi in ⊢ (???%); >div_plus_times /2 by refl, monotonic_lt_minus_l, trans_eq/ 
+  ]
 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)
+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 //
+   normalize <assoc <assoc in ⊢ (???%); @eq_f >assoc >comm in ⊢ (??(????%?)?);
+   <assoc @eq_f @Hind
+  |>bigop_Sfalse // >bigop_Sfalse // >bigop_Sfalse //
   ]
 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
+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)=
+    op (f i) (\big[op,nil]_{x<n|andb(notb(eqb i x))(p x)}(f x)).
+#p #B #nil #op #f #i #n (elim n) 
+  [#ltO @False_ind /2/
+  |#n #Hind #lein #pi cases (le_to_or_lt_eq … (le_S_S_to_le …lein)) #Hi
+    [cut (andb(notb(eqb i n))(p n) = (p n))
+      [>(not_eq_to_eqb_false … (lt_to_not_eq … Hi)) //] #Hcut
+     cases (true_or_false (p n)) #pn 
+      [>bigop_Strue // >bigop_Strue //
+       normalize >assoc >(comm ?? op (f i) (f n)) <assoc >Hind //
+      |>bigop_Sfalse // >bigop_Sfalse // >Hind //  
+      ]
+    |<Hi >bigop_Strue // @eq_f >bigop_Sfalse  
+       [@same_bigop // #k #ltki >not_eq_to_eqb_false /2/
+       |>eq_to_eqb_true // 
+       ]
      ]
-   |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
+(* range *)
+record range (A:Type[0]): Type[0] ≝
+  {enum:nat→A; upto:nat; filter:nat→bool}.
   
-    [intros.
-     elim (divides_b (x/S m) n);reflexivity
-    |intros.reflexivity
-    ]
-  ]
-|elim H1.apply lt_to_le.assumption
-]
+definition sub_hk: (nat→nat)→(nat→nat)→∀A:Type[0].relation (range A) ≝
+λh,k,A,I,J.∀i.i<(upto A I) → (filter A I i)=true → 
+  (h i < upto A J
+  ∧ filter A J (h i) = true
+  ∧ k (h i) = i).
+
+definition iso: ∀A:Type[0].relation (range A) ≝
+  λA,I,J.∃h,k. 
+    (∀i. i < (upto A I) → (filter A I i) = true → 
+       enum A I i = enum A J (h i)) ∧
+    sub_hk h k A I J ∧ sub_hk k h A J I.
+  
+lemma sub_hkO: ∀h,k,A,I,J. upto A I = 0 → sub_hk h k A I J.
+#h #k #A #I #J #up0 #i #lti >up0 @False_ind /2/
 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
-    ]
-  ]
-]
+lemma sub0_to_false: ∀h,k,A,I,J. upto A I = 0 → sub_hk h k A J I → 
+  ∀i. i < upto A J → filter A J i = false.
+#h #k #A #I #J #up0 #sub #i #lti cases(true_or_false (filter A J i)) //
+#ptrue (cases (sub i lti ptrue)) * #hi @False_ind /2/ 
 qed.
 
-(* old version - proved without theorem iter_p_gen_knm
-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).
-rewrite < (iter_p_gen2' ? ? ? ? ? ? ? ? H H1 H2).
-apply sym_eq.
-letin h := (\lambda x.(h11 (x/m2) (x\mod m2))*m1 + (h12 (x/m2) (x\mod m2))).
-letin h1 := (\lambda x.(h21 (x/m1) (x\mod m1))*m2 + (h22 (x/m1) (x\mod m1))).
-apply (trans_eq ? ? 
-  (iter_p_gen (n2*m2) (\lambda x:nat.p21 (x/m2)\land p22 (x/m2) (x\mod m2)) A
-  (\lambda x:nat.g ((h x)/m1) ((h x)\mod m1)) baseA plusA ))
-  [clear h.clear h1.
-   apply eq_iter_p_gen1
-    [intros.reflexivity
-    |intros.
-     cut (O < m2)
-      [cut (x/m2 < n2)
-        [cut (x \mod m2 < m2)
-          [elim (and_true ? ? H6).
-           elim (H3 ? ? Hcut1 Hcut2 H7 H8).
-           elim H9.clear H9.
-           elim H11.clear H11.
-           elim H9.clear H9.
-           elim H11.clear H11.
-           apply eq_f2
-            [apply sym_eq.
-             apply div_plus_times.
-             assumption
-            | apply sym_eq.
-              apply mod_plus_times.
-              assumption
-            ]
-          |apply lt_mod_m_m.
-           assumption
-          ]
-        |apply (lt_times_n_to_lt m2)
-          [assumption
-          |apply (le_to_lt_to_lt ? x)
-            [apply (eq_plus_to_le ? ? (x \mod m2)).
-             apply div_mod.
-             assumption
-            |assumption
-            ]
-          ]
-        ]
-      |apply not_le_to_lt.unfold.intro.
-       generalize in match H5.
-       apply (le_n_O_elim ? H7).
-       rewrite < times_n_O.
-       apply le_to_not_lt.
-       apply le_O_n  
-      ]      
+lemma sub_lt: ∀A,e,p,n,m. n ≤ m → 
+  sub_hk (λx.x) (λx.x) A (mk_range A e n p) (mk_range A e m p).
+#A #e #f #n #m #lenm #i #lti #fi % // % /2 by lt_to_le_to_lt/
+qed. 
+
+theorem transitive_sub: ∀h1,k1,h2,k2,A,I,J,K. 
+  sub_hk h1 k1 A I J → sub_hk h2 k2 A J K → 
+    sub_hk (λx.h2(h1 x)) (λx.k1(k2 x)) A I K.
+#h1 #k1 #h2 #k2 #A #I #J #K #sub1 #sub2 #i #lti #fi 
+cases(sub1 i lti fi) * #lth1i #fh1i #ei 
+cases(sub2 (h1 i) lth1i fh1i) * #H1 #H2 #H3 % // % // 
+qed. 
+
+theorem bigop_iso: ∀n1,n2,p1,p2,B.∀nil.∀op:ACop B nil.∀f1,f2.
+  iso B (mk_range B f1 n1 p1) (mk_range B f2 n2 p2) →
+  \big[op,nil]_{i<n1|p1 i}(f1 i) = \big[op,nil]_{i<n2|p2 i}(f2 i).
+#n1 #n2 #p1 #p2 #B #nil #op #f1 #f2 * #h * #k * * #same
+@(le_gen ? n1) #i lapply p2 (elim i) 
+  [(elim n2) // #m #Hind #p2 #_ #sub1 #sub2
+   >bigop_Sfalse 
+    [@(Hind ? (le_O_n ?)) [/2/ | @(transitive_sub … (sub_lt …) sub2) //]
+    |@(sub0_to_false … sub2) //
     ]
-  |apply (eq_iter_p_gen_gh ? ? ? H H1 H2 ? h h1);intros
-    [cut (O < m2)
-      [cut (i/m2 < n2)
-        [cut (i \mod m2 < m2)
-          [elim (and_true ? ? H6).
-           elim (H3 ? ? Hcut1 Hcut2 H7 H8).
-           elim H9.clear H9.
-           elim H11.clear H11.
-           elim H9.clear H9.
-           elim H11.clear H11.
-           cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))/m1 = 
-                 h11 (i/m2) (i\mod m2))
-            [cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))\mod m1 =
-                  h12 (i/m2) (i\mod m2))
-              [rewrite > Hcut3.
-               rewrite > Hcut4.
-               rewrite > H9.
-               rewrite > H15.
-               reflexivity
-              |apply mod_plus_times. 
-               assumption
-              ]
-            |apply div_plus_times.
-             assumption
-            ]
-          |apply lt_mod_m_m.
-           assumption
-          ]
-        |apply (lt_times_n_to_lt m2)
-          [assumption
-          |apply (le_to_lt_to_lt ? i)
-            [apply (eq_plus_to_le ? ? (i \mod m2)).
-             apply div_mod.
-             assumption
-            |assumption
-            ]
-          ]
-        ]
-      |apply not_le_to_lt.unfold.intro.
-       generalize in match H5.
-       apply (le_n_O_elim ? H7).
-       rewrite < times_n_O.
-       apply le_to_not_lt.
-       apply le_O_n  
-      ]      
-    |cut (O < m2)
-      [cut (i/m2 < n2)
-        [cut (i \mod m2 < m2)
-          [elim (and_true ? ? H6).
-           elim (H3 ? ? Hcut1 Hcut2 H7 H8).
-           elim H9.clear H9.
-           elim H11.clear H11.
-           elim H9.clear H9.
-           elim H11.clear H11.
-           cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))/m1 = 
-                 h11 (i/m2) (i\mod m2))
-            [cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))\mod m1 =
-                  h12 (i/m2) (i\mod m2))
-              [rewrite > Hcut3.
-               rewrite > Hcut4.
-               rewrite > H13.
-               rewrite > H14.
-               apply sym_eq.
-               apply div_mod.
-               assumption
-              |apply mod_plus_times. 
-               assumption
-              ]
-            |apply div_plus_times.
-             assumption
-            ]
-          |apply lt_mod_m_m.
-           assumption
-          ]
-        |apply (lt_times_n_to_lt m2)
-          [assumption
-          |apply (le_to_lt_to_lt ? i)
-            [apply (eq_plus_to_le ? ? (i \mod m2)).
-             apply div_mod.
-             assumption
-            |assumption
-            ]
-          ]
-        ]
-      |apply not_le_to_lt.unfold.intro.
-       generalize in match H5.
-       apply (le_n_O_elim ? H7).
-       rewrite < times_n_O.
-       apply le_to_not_lt.
-       apply le_O_n  
-      ]      
-    |cut (O < m2)
-      [cut (i/m2 < n2)
-        [cut (i \mod m2 < m2)
-          [elim (and_true ? ? H6).
-           elim (H3 ? ? Hcut1 Hcut2 H7 H8).
-           elim H9.clear H9.
-           elim H11.clear H11.
-           elim H9.clear H9.
-           elim H11.clear H11.
-           apply lt_times_plus_times
-            [assumption|assumption]
-          |apply lt_mod_m_m.
-           assumption
-          ]
-        |apply (lt_times_n_to_lt m2)
-          [assumption
-          |apply (le_to_lt_to_lt ? i)
-            [apply (eq_plus_to_le ? ? (i \mod m2)).
-             apply div_mod.
-             assumption
-            |assumption
-            ]
-          ]
-        ]
-      |apply not_le_to_lt.unfold.intro.
-       generalize in match H5.
-       apply (le_n_O_elim ? H7).
-       rewrite < times_n_O.
-       apply le_to_not_lt.
-       apply le_O_n  
+  |#n #Hind #p2 #ltn #sub1 #sub2 (cut (n ≤n1)) [/2/] #len
+   cases(true_or_false (p1 n)) #p1n
+    [>bigop_Strue // (cases (sub1 n (le_n …) p1n)) * #hn #p2hn #eqn
+     >(bigop_diff … (h n) n2) // >same // 
+     @eq_f @(Hind ? len)
+      [#i #ltin #p1i (cases (sub1 i (le_S … ltin) p1i)) * 
+       #h1i #p2h1i #eqi % // % // >not_eq_to_eqb_false normalize // 
+       @(not_to_not ??? (lt_to_not_eq ? ? ltin)) // 
+      |#j #ltj #p2j (cases (sub2 j ltj (andb_true_r …p2j))) * 
+       #ltkj #p1kj #eqj % // % // 
+       (cases (le_to_or_lt_eq …(le_S_S_to_le …ltkj))) //
+       #eqkj @False_ind lapply p2j @eqb_elim 
+       normalize /2/
       ]
-    |cut (O < m1)
-      [cut (j/m1 < n1)
-        [cut (j \mod m1 < m1)
-          [elim (and_true ? ? H6).
-           elim (H4 ? ? Hcut1 Hcut2 H7 H8).
-           elim H9.clear H9.
-           elim H11.clear H11.
-           elim H9.clear H9.
-           elim H11.clear H11.
-           cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))/m2 = 
-                 h21 (j/m1) (j\mod m1))
-            [cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))\mod m2 =
-                  h22 (j/m1) (j\mod m1))
-              [rewrite > Hcut3.
-               rewrite > Hcut4.
-               rewrite > H9.
-               rewrite > H15.
-               reflexivity
-              |apply mod_plus_times. 
-               assumption
-              ]
-            |apply div_plus_times.
-             assumption
-            ]
-          |apply lt_mod_m_m.
-           assumption
-          ] 
-        |apply (lt_times_n_to_lt m1)
-          [assumption
-          |apply (le_to_lt_to_lt ? j)
-            [apply (eq_plus_to_le ? ? (j \mod m1)).
-             apply div_mod.
-             assumption
-            |assumption
-            ]
-          ]
-        ]
-      |apply not_le_to_lt.unfold.intro.
-       generalize in match H5.
-       apply (le_n_O_elim ? H7).
-       rewrite < times_n_O.
-       apply le_to_not_lt.
-       apply le_O_n  
-      ] 
-    |cut (O < m1)
-      [cut (j/m1 < n1)
-        [cut (j \mod m1 < m1)
-          [elim (and_true ? ? H6).
-           elim (H4 ? ? Hcut1 Hcut2 H7 H8).
-           elim H9.clear H9.
-           elim H11.clear H11.
-           elim H9.clear H9.
-           elim H11.clear H11.
-           cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))/m2 = 
-                 h21 (j/m1) (j\mod m1))
-            [cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))\mod m2 =
-                  h22 (j/m1) (j\mod m1))
-              [rewrite > Hcut3.
-               rewrite > Hcut4.               
-               rewrite > H13.
-               rewrite > H14.
-               apply sym_eq.
-               apply div_mod.
-               assumption
-              |apply mod_plus_times. 
-               assumption
-              ]
-            |apply div_plus_times.
-             assumption
-            ]
-          |apply lt_mod_m_m.
-           assumption
-          ] 
-        |apply (lt_times_n_to_lt m1)
-          [assumption
-          |apply (le_to_lt_to_lt ? j)
-            [apply (eq_plus_to_le ? ? (j \mod m1)).
-             apply div_mod.
-             assumption
-            |assumption
-            ]
-          ]
-        ]
-      |apply not_le_to_lt.unfold.intro.
-       generalize in match H5.
-       apply (le_n_O_elim ? H7).
-       rewrite < times_n_O.
-       apply le_to_not_lt.
-       apply le_O_n  
-      ] 
-    |cut (O < m1)
-      [cut (j/m1 < n1)
-        [cut (j \mod m1 < m1)
-          [elim (and_true ? ? H6).
-           elim (H4 ? ? Hcut1 Hcut2 H7 H8).
-           elim H9.clear H9.
-           elim H11.clear H11.
-           elim H9.clear H9.
-           elim H11.clear H11.
-           apply (lt_times_plus_times ? ? ? m2)
-            [assumption|assumption]
-          |apply lt_mod_m_m.
-           assumption
-          ] 
-        |apply (lt_times_n_to_lt m1)
-          [assumption
-          |apply (le_to_lt_to_lt ? j)
-            [apply (eq_plus_to_le ? ? (j \mod m1)).
-             apply div_mod.
-             assumption
-            |assumption
-            ]
-          ]
-        ]
-      |apply not_le_to_lt.unfold.intro.
-       generalize in match H5.
-       apply (le_n_O_elim ? H7).
-       rewrite < times_n_O.
-       apply le_to_not_lt.
-       apply le_O_n  
-      ]
-    ]
-  ]
-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
+    |>bigop_Sfalse // @(Hind ? len) 
+      [@(transitive_sub … (sub_lt …) sub1) //
+      |#i #lti #p2i cases(sub2 i lti p2i) * #ltki #p1ki #eqi
+       % // % // cases(le_to_or_lt_eq …(le_S_S_to_le …ltki)) //
+       #eqki @False_ind /2/
       ]
     ]
   ]
-]
 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
+(* commutation *)
+theorem bigop_commute: ∀n,m,p11,p12,p21,p22,B.∀nil.∀op:ACop B nil.∀f.
+0 < n → 0 < m →
+(∀i,j. i < n → j < m → (p11 i ∧ p12 i j) = (p21 j ∧ p22 i j)) →
+\big[op,nil]_{i<n|p11 i}(\big[op,nil]_{j<m|p12 i j}(f i j)) =
+   \big[op,nil]_{j<m|p21 j}(\big[op,nil]_{i<n|p22 i j}(f i j)).
+#n #m #p11 #p12 #p21 #p22 #B #nil #op #f #posn #posm #Heq
+>bigop_prod >bigop_prod @bigop_iso 
+%{(λi.(i\mod m)*n + i/m)} %{(λi.(i\mod n)*m + i/n)} % 
+  [% 
+    [#i #lti #Heq (* whd in ⊢ (???(?(?%?)?)); *) @eq_f2
+      [@sym_eq @mod_plus_times /2 by lt_times_to_lt_div/
+      |@sym_eq @div_plus_times /2 by lt_times_to_lt_div/
+      ]
+    |#i #lti #Hi 
+     cut ((i\mod m*n+i/m)\mod n=i/m)
+      [@mod_plus_times @lt_times_to_lt_div //] #H1
+     cut ((i\mod m*n+i/m)/n=i \mod m)
+      [@div_plus_times @lt_times_to_lt_div //] #H2
+     %[%[@(lt_to_le_to_lt ? (i\mod m*n+n))
+          [whd >plus_n_Sm @monotonic_le_plus_r @lt_times_to_lt_div //
+          |>commutative_plus @(le_times (S(i \mod m)) m n n) // @lt_mod_m_m //
+          ]
+        |lapply (Heq (i/m) (i \mod m) ??)
+          [@lt_mod_m_m // |@lt_times_to_lt_div //|>Hi >H1 >H2 //]
+        ]
+      |>H1 >H2 //
       ]
-    |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
+  |#i #lti #Hi 
+   cut ((i\mod n*m+i/n)\mod m=i/n)
+    [@mod_plus_times @lt_times_to_lt_div //] #H1
+   cut ((i\mod n*m+i/n)/m=i \mod n)
+    [@div_plus_times @lt_times_to_lt_div //] #H2
+   %[%[@(lt_to_le_to_lt ? (i\mod n*m+m))
+        [whd >plus_n_Sm @monotonic_le_plus_r @lt_times_to_lt_div //
+        |>commutative_plus @(le_times (S(i \mod n)) n m m) // @lt_mod_m_m //
+        ]
+      |lapply (Heq (i \mod n) (i/n) ??)
+        [@lt_times_to_lt_div // |@lt_mod_m_m // |>Hi >H1 >H2 //]
       ]
-    |assumption
+    |>H1 >H2 //
     ]
   ]
-qed.
\ No newline at end of file
+qed.
+   
+(* 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.∀f,a.
+  let aop ≝ sum B nil R in
+  let mop ≝ 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.