From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 22 May 2019 13:43:08 +0200 Subject: htmldoc regenerated --- docs/htmldoc/mathcomp.ssreflect.bigop.html | 1132 +++++++++++++++------------- 1 file changed, 589 insertions(+), 543 deletions(-) (limited to 'docs/htmldoc/mathcomp.ssreflect.bigop.html') diff --git a/docs/htmldoc/mathcomp.ssreflect.bigop.html b/docs/htmldoc/mathcomp.ssreflect.bigop.html index dce0b01..97f9fcd 100644 --- a/docs/htmldoc/mathcomp.ssreflect.bigop.html +++ b/docs/htmldoc/mathcomp.ssreflect.bigop.html @@ -21,7 +21,6 @@
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.

@@ -387,56 +386,56 @@
Structure law := Law {
-  operator : T → T → T;
-  _ : associative operator;
-  _ : left_id idm operator;
-  _ : right_id idm operator
+  operator : T → T → T;
+  _ : associative operator;
+  _ : left_id idm operator;
+  _ : right_id idm operator
}.

Structure com_law := ComLaw {
   com_operator : law;
-   _ : commutative com_operator
+   _ : commutative com_operator
}.

Structure mul_law := MulLaw {
-  mul_operator : T → T → T;
-  _ : left_zero idm mul_operator;
-  _ : right_zero idm mul_operator
+  mul_operator : T → T → T;
+  _ : left_zero idm mul_operator;
+  _ : right_zero idm mul_operator
}.

-Structure add_law (mul : T → T → T) := AddLaw {
+Structure add_law (mul : T → T → T) := AddLaw {
  add_operator : com_law;
-  _ : left_distributive mul add_operator;
-  _ : right_distributive mul add_operator
+  _ : left_distributive mul add_operator;
+  _ : right_distributive mul add_operator
}.

-Let op_id (op1 op2 : T → T → T) := phant_id op1 op2.
+Let op_id (op1 op2 : T → T → T) := phant_id op1 op2.

Definition clone_law op :=
  fun (opL : law) & op_id opL op ⇒
  fun opmA op1m opm1 (opL' := @Law op opmA op1m opm1)
-    & phant_id opL' opL ⇒ opL'.
+    & phant_id opL' opL ⇒ opL'.

Definition clone_com_law op :=
  fun (opL : law) (opC : com_law) & op_id opL op & op_id opC op ⇒
-  fun opmC (opC' := @ComLaw opL opmC) & phant_id opC' opC ⇒ opC'.
+  fun opmC (opC' := @ComLaw opL opmC) & phant_id opC' opC ⇒ opC'.

Definition clone_mul_law op :=
  fun (opM : mul_law) & op_id opM op ⇒
-  fun op0m opm0 (opM' := @MulLaw op op0m opm0) & phant_id opM' opM ⇒ opM'.
+  fun op0m opm0 (opM' := @MulLaw op op0m opm0) & phant_id opM' opM ⇒ opM'.

Definition clone_add_law mop aop :=
  fun (opC : com_law) (opA : add_law mop) & op_id opC aop & op_id opA aop ⇒
  fun mopDm mopmD (opA' := @AddLaw mop opC mopDm mopmD)
-    & phant_id opA' opA ⇒ opA'.
+    & phant_id opA' opA ⇒ opA'.

End Definitions.
@@ -447,13 +446,13 @@ Coercion com_operator : com_law >-> law.
Coercion mul_operator : mul_law >-> Funclass.
Coercion add_operator : add_law >-> com_law.
-Notation "[ 'law' 'of' f ]" := (@clone_law _ _ f _ id _ _ _ id)
+Notation "[ 'law' 'of' f ]" := (@clone_law _ _ f _ id _ _ _ id)
  (at level 0, format"[ 'law' 'of' f ]") : form_scope.
-Notation "[ 'com_law' 'of' f ]" := (@clone_com_law _ _ f _ _ id id _ id)
+Notation "[ 'com_law' 'of' f ]" := (@clone_com_law _ _ f _ _ id id _ id)
  (at level 0, format "[ 'com_law' 'of' f ]") : form_scope.
-Notation "[ 'mul_law' 'of' f ]" := (@clone_mul_law _ _ f _ id _ _ id)
+Notation "[ 'mul_law' 'of' f ]" := (@clone_mul_law _ _ f _ id _ _ id)
  (at level 0, format"[ 'mul_law' 'of' f ]") : form_scope.
-Notation "[ 'add_law' m 'of' a ]" := (@clone_add_law _ _ m a _ _ id id _ _ id)
+Notation "[ 'add_law' m 'of' a ]" := (@clone_add_law _ _ m a _ _ id id _ _ id)
  (at level 0, format "[ 'add_law' m 'of' a ]") : form_scope.
End Exports.
@@ -461,17 +460,17 @@ Section CommutativeAxioms.

-Variable (T : Type) (zero one : T) (mul add : T → T → T) (inv : T → T).
-Hypothesis mulC : commutative mul.
+Variable (T : Type) (zero one : T) (mul add : T → T → T) (inv : T → T).
+Hypothesis mulC : commutative mul.

-Lemma mulC_id : left_id one mul → right_id one mul.
+Lemma mulC_id : left_id one mul → right_id one mul.

-Lemma mulC_zero : left_zero zero mul → right_zero zero mul.
+Lemma mulC_zero : left_zero zero mul → right_zero zero mul.

-Lemma mulC_dist : left_distributive mul add → right_distributive mul add.
+Lemma mulC_dist : left_distributive mul add → right_distributive mul add.

End CommutativeAxioms.
@@ -486,43 +485,43 @@
Section Plain.
Variable mul : law idm.
-Lemma mul1m : left_id idm mul.
-Lemma mulm1 : right_id idm mul.
-Lemma mulmA : associative mul.
-Lemma iteropE n x : iterop n mul x idm = iter n (mul x) idm.
+Lemma mul1m : left_id idm mul.
+Lemma mulm1 : right_id idm mul.
+Lemma mulmA : associative mul.
+Lemma iteropE n x : iterop n mul x idm = iter n (mul x) idm.
End Plain.

Section Commutative.
Variable mul : com_law idm.
-Lemma mulmC : commutative mul.
-Lemma mulmCA : left_commutative mul.
- Lemma mulmAC : right_commutative mul.
- Lemma mulmACA : interchange mul mul.
+Lemma mulmC : commutative mul.
+Lemma mulmCA : left_commutative mul.
+ Lemma mulmAC : right_commutative mul.
+ Lemma mulmACA : interchange mul mul.
End Commutative.

Section Mul.
Variable mul : mul_law idm.
-Lemma mul0m : left_zero idm mul.
-Lemma mulm0 : right_zero idm mul.
+Lemma mul0m : left_zero idm mul.
+Lemma mulm0 : right_zero idm mul.
End Mul.

Section Add.
-Variables (mul : T → T → T) (add : add_law idm mul).
-Lemma addmA : associative add.
-Lemma addmC : commutative add.
-Lemma addmCA : left_commutative add.
-Lemma addmAC : right_commutative add.
-Lemma add0m : left_id idm add.
-Lemma addm0 : right_id idm add.
-Lemma mulm_addl : left_distributive mul add.
-Lemma mulm_addr : right_distributive mul add.
+Variables (mul : T → T → T) (add : add_law idm mul).
+Lemma addmA : associative add.
+Lemma addmC : commutative add.
+Lemma addmCA : left_commutative add.
+Lemma addmAC : right_commutative add.
+Lemma add0m : left_id idm add.
+Lemma addm0 : right_id idm add.
+Lemma mulm_addl : left_distributive mul add.
+Lemma mulm_addr : right_distributive mul add.
End Add.

-Definition simpm := (mulm1, mulm0, mul1m, mul0m, mulmA).
+Definition simpm := (mulm1, mulm0, mul1m, mul0m, mulmA).

End Theory.
@@ -542,19 +541,19 @@ Import Monoid.

-Canonical andb_monoid := Law andbA andTb andbT.
-Canonical andb_comoid := ComLaw andbC.
+Canonical andb_monoid := Law andbA andTb andbT.
+Canonical andb_comoid := ComLaw andbC.

-Canonical andb_muloid := MulLaw andFb andbF.
-Canonical orb_monoid := Law orbA orFb orbF.
-Canonical orb_comoid := ComLaw orbC.
-Canonical orb_muloid := MulLaw orTb orbT.
-Canonical addb_monoid := Law addbA addFb addbF.
-Canonical addb_comoid := ComLaw addbC.
-Canonical orb_addoid := AddLaw andb_orl andb_orr.
-Canonical andb_addoid := AddLaw orb_andl orb_andr.
-Canonical addb_addoid := AddLaw andb_addl andb_addr.
+Canonical andb_muloid := MulLaw andFb andbF.
+Canonical orb_monoid := Law orbA orFb orbF.
+Canonical orb_comoid := ComLaw orbC.
+Canonical orb_muloid := MulLaw orTb orbT.
+Canonical addb_monoid := Law addbA addFb addbF.
+Canonical addb_comoid := ComLaw addbC.
+Canonical orb_addoid := AddLaw andb_orl andb_orr.
+Canonical andb_addoid := AddLaw orb_andl orb_andr.
+Canonical addb_addoid := AddLaw andb_addl andb_addr.

Canonical addn_monoid := Law addnA add0n addn0.
@@ -617,159 +616,159 @@ Print Canonical Projections. the <general_term>, thus allowing for the insertion of coercions.
-CoInductive bigbody R I := BigBody of I & (R → R → R) & bool & R.
+Variant bigbody R I := BigBody of I & (R → R → R) & bool & R.

Definition applybig {R I} (body : bigbody R I) x :=
-  let: BigBody _ op b v := body in if b then op v x else x.
+  let: BigBody _ op b v := body in if b then op v x else x.

-Definition reducebig R I idx r (body : I → bigbody R I) :=
-  foldr (applybig \o body) idx r.
+Definition reducebig R I idx r (body : I → bigbody R I) :=
+  foldr (applybig \o body) idx r.

Module Type BigOpSig.
-Parameter bigop : ∀ R I, R → seq I → (I → bigbody R I) → R.
-Axiom bigopE : bigop = reducebig.
+Parameter bigop : ∀ R I, R → seq I → (I → bigbody R I) → R.
+Axiom bigopE : bigop = reducebig.
End BigOpSig.

Module BigOp : BigOpSig.
Definition bigop := reducebig.
-Lemma bigopE : bigop = reducebig.
+Lemma bigopE : bigop = reducebig.
End BigOp.

Notation bigop := BigOp.bigop (only parsing).
-Canonical bigop_unlock := Unlockable BigOp.bigopE.
+Canonical bigop_unlock := Unlockable BigOp.bigopE.

-Definition index_iota m n := iota m (n - m).
+Definition index_iota m n := iota m (n - m).

Definition index_enum (T : finType) := Finite.enum T.

-Lemma mem_index_iota m n i : i \in index_iota m n = (m ≤ i < n).
+Lemma mem_index_iota m n i : i \in index_iota m n = (m ≤ i < n).

-Lemma mem_index_enum T i : i \in index_enum T.
- Hint Resolve mem_index_enum.
+Lemma mem_index_enum T i : i \in index_enum T.
+ Hint Resolve mem_index_enum : core.

-Lemma filter_index_enum T P : filter P (index_enum T) = enum P.
+Lemma filter_index_enum T P : filter P (index_enum T) = enum P.

-Notation "\big [ op / idx ]_ ( i <- r | P ) F" :=
+Notation "\big [ op / idx ]_ ( i <- r | P ) F" :=
  (bigop idx r (fun i ⇒ BigBody i op P%B F)) : big_scope.
-Notation "\big [ op / idx ]_ ( i <- r ) F" :=
-  (bigop idx r (fun i ⇒ BigBody i op true F)) : big_scope.
-Notation "\big [ op / idx ]_ ( m <= i < n | P ) F" :=
-  (bigop idx (index_iota m n) (fun i : nat ⇒ BigBody i op P%B F))
+Notation "\big [ op / idx ]_ ( i <- r ) F" :=
+  (bigop idx r (fun i ⇒ BigBody i op true F)) : big_scope.
+Notation "\big [ op / idx ]_ ( m <= i < n | P ) F" :=
+  (bigop idx (index_iota m n) (fun i : nat ⇒ BigBody i op P%B F))
     : big_scope.
-Notation "\big [ op / idx ]_ ( m <= i < n ) F" :=
-  (bigop idx (index_iota m n) (fun i : nat ⇒ BigBody i op true F))
+Notation "\big [ op / idx ]_ ( m <= i < n ) F" :=
+  (bigop idx (index_iota m n) (fun i : nat ⇒ BigBody i op true F))
     : big_scope.
-Notation "\big [ op / idx ]_ ( i | P ) F" :=
+Notation "\big [ op / idx ]_ ( i | P ) F" :=
  (bigop idx (index_enum _) (fun i ⇒ BigBody i op P%B F)) : big_scope.
-Notation "\big [ op / idx ]_ i F" :=
-  (bigop idx (index_enum _) (fun i ⇒ BigBody i op true F)) : big_scope.
-Notation "\big [ op / idx ]_ ( i : t | P ) F" :=
+Notation "\big [ op / idx ]_ i F" :=
+  (bigop idx (index_enum _) (fun i ⇒ BigBody i op true F)) : big_scope.
+Notation "\big [ op / idx ]_ ( i : t | P ) F" :=
  (bigop idx (index_enum _) (fun i : t ⇒ BigBody i op P%B F))
     (only parsing) : big_scope.
-Notation "\big [ op / idx ]_ ( i : t ) F" :=
-  (bigop idx (index_enum _) (fun i : t ⇒ BigBody i op true F))
+Notation "\big [ op / idx ]_ ( i : t ) F" :=
+  (bigop idx (index_enum _) (fun i : t ⇒ BigBody i op true F))
     (only parsing) : big_scope.
-Notation "\big [ op / idx ]_ ( i < n | P ) F" :=
-  (\big[op/idx]_(i : ordinal n | P%B) F) : big_scope.
-Notation "\big [ op / idx ]_ ( i < n ) F" :=
-  (\big[op/idx]_(i : ordinal n) F) : big_scope.
-Notation "\big [ op / idx ]_ ( i 'in' A | P ) F" :=
-  (\big[op/idx]_(i | (i \in A) && P) F) : big_scope.
-Notation "\big [ op / idx ]_ ( i 'in' A ) F" :=
-  (\big[op/idx]_(i | i \in A) F) : big_scope.
- -
-Notation BIG_F := (F in \big[_/_]_(i <- _ | _) F i)%pattern.
-Notation BIG_P := (P in \big[_/_]_(i <- _ | P i) _)%pattern.
- -
-Notation "\sum_ ( i <- r | P ) F" :=
-  (\big[+%N/0%N]_(i <- r | P%B) F%N) : nat_scope.
-Notation "\sum_ ( i <- r ) F" :=
-  (\big[+%N/0%N]_(i <- r) F%N) : nat_scope.
-Notation "\sum_ ( m <= i < n | P ) F" :=
-  (\big[+%N/0%N]_(m ≤ i < n | P%B) F%N) : nat_scope.
-Notation "\sum_ ( m <= i < n ) F" :=
-  (\big[+%N/0%N]_(m ≤ i < n) F%N) : nat_scope.
-Notation "\sum_ ( i | P ) F" :=
-  (\big[+%N/0%N]_(i | P%B) F%N) : nat_scope.
-Notation "\sum_ i F" :=
-  (\big[+%N/0%N]_i F%N) : nat_scope.
-Notation "\sum_ ( i : t | P ) F" :=
-  (\big[+%N/0%N]_(i : t | P%B) F%N) (only parsing) : nat_scope.
-Notation "\sum_ ( i : t ) F" :=
-  (\big[+%N/0%N]_(i : t) F%N) (only parsing) : nat_scope.
-Notation "\sum_ ( i < n | P ) F" :=
-  (\big[+%N/0%N]_(i < n | P%B) F%N) : nat_scope.
-Notation "\sum_ ( i < n ) F" :=
-  (\big[+%N/0%N]_(i < n) F%N) : nat_scope.
-Notation "\sum_ ( i 'in' A | P ) F" :=
-  (\big[+%N/0%N]_(i in A | P%B) F%N) : nat_scope.
-Notation "\sum_ ( i 'in' A ) F" :=
-  (\big[+%N/0%N]_(i in A) F%N) : nat_scope.
- -
-Notation "\prod_ ( i <- r | P ) F" :=
-  (\big[*%N/1%N]_(i <- r | P%B) F%N) : nat_scope.
-Notation "\prod_ ( i <- r ) F" :=
-  (\big[*%N/1%N]_(i <- r) F%N) : nat_scope.
-Notation "\prod_ ( m <= i < n | P ) F" :=
-  (\big[*%N/1%N]_(m ≤ i < n | P%B) F%N) : nat_scope.
-Notation "\prod_ ( m <= i < n ) F" :=
-  (\big[*%N/1%N]_(m ≤ i < n) F%N) : nat_scope.
-Notation "\prod_ ( i | P ) F" :=
-  (\big[*%N/1%N]_(i | P%B) F%N) : nat_scope.
-Notation "\prod_ i F" :=
-  (\big[*%N/1%N]_i F%N) : nat_scope.
-Notation "\prod_ ( i : t | P ) F" :=
-  (\big[*%N/1%N]_(i : t | P%B) F%N) (only parsing) : nat_scope.
-Notation "\prod_ ( i : t ) F" :=
-  (\big[*%N/1%N]_(i : t) F%N) (only parsing) : nat_scope.
-Notation "\prod_ ( i < n | P ) F" :=
-  (\big[*%N/1%N]_(i < n | P%B) F%N) : nat_scope.
-Notation "\prod_ ( i < n ) F" :=
-  (\big[*%N/1%N]_(i < n) F%N) : nat_scope.
-Notation "\prod_ ( i 'in' A | P ) F" :=
-  (\big[*%N/1%N]_(i in A | P%B) F%N) : nat_scope.
-Notation "\prod_ ( i 'in' A ) F" :=
-  (\big[*%N/1%N]_(i in A) F%N) : nat_scope.
- -
-Notation "\max_ ( i <- r | P ) F" :=
-  (\big[maxn/0%N]_(i <- r | P%B) F%N) : nat_scope.
-Notation "\max_ ( i <- r ) F" :=
-  (\big[maxn/0%N]_(i <- r) F%N) : nat_scope.
-Notation "\max_ ( i | P ) F" :=
-  (\big[maxn/0%N]_(i | P%B) F%N) : nat_scope.
-Notation "\max_ i F" :=
-  (\big[maxn/0%N]_i F%N) : nat_scope.
-Notation "\max_ ( i : I | P ) F" :=
-  (\big[maxn/0%N]_(i : I | P%B) F%N) (only parsing) : nat_scope.
-Notation "\max_ ( i : I ) F" :=
-  (\big[maxn/0%N]_(i : I) F%N) (only parsing) : nat_scope.
-Notation "\max_ ( m <= i < n | P ) F" :=
- (\big[maxn/0%N]_(m ≤ i < n | P%B) F%N) : nat_scope.
-Notation "\max_ ( m <= i < n ) F" :=
- (\big[maxn/0%N]_(m ≤ i < n) F%N) : nat_scope.
-Notation "\max_ ( i < n | P ) F" :=
- (\big[maxn/0%N]_(i < n | P%B) F%N) : nat_scope.
-Notation "\max_ ( i < n ) F" :=
- (\big[maxn/0%N]_(i < n) F%N) : nat_scope.
-Notation "\max_ ( i 'in' A | P ) F" :=
- (\big[maxn/0%N]_(i in A | P%B) F%N) : nat_scope.
-Notation "\max_ ( i 'in' A ) F" :=
- (\big[maxn/0%N]_(i in A) F%N) : nat_scope.
+Notation "\big [ op / idx ]_ ( i < n | P ) F" :=
+  (\big[op/idx]_(i : ordinal n | P%B) F) : big_scope.
+Notation "\big [ op / idx ]_ ( i < n ) F" :=
+  (\big[op/idx]_(i : ordinal n) F) : big_scope.
+Notation "\big [ op / idx ]_ ( i 'in' A | P ) F" :=
+  (\big[op/idx]_(i | (i \in A) && P) F) : big_scope.
+Notation "\big [ op / idx ]_ ( i 'in' A ) F" :=
+  (\big[op/idx]_(i | i \in A) F) : big_scope.
+ +
+Notation BIG_F := (F in \big[_/_]_(i <- _ | _) F i)%pattern.
+Notation BIG_P := (P in \big[_/_]_(i <- _ | P i) _)%pattern.
+ +
+Notation "\sum_ ( i <- r | P ) F" :=
+  (\big[+%N/0%N]_(i <- r | P%B) F%N) : nat_scope.
+Notation "\sum_ ( i <- r ) F" :=
+  (\big[+%N/0%N]_(i <- r) F%N) : nat_scope.
+Notation "\sum_ ( m <= i < n | P ) F" :=
+  (\big[+%N/0%N]_(m ≤ i < n | P%B) F%N) : nat_scope.
+Notation "\sum_ ( m <= i < n ) F" :=
+  (\big[+%N/0%N]_(m ≤ i < n) F%N) : nat_scope.
+Notation "\sum_ ( i | P ) F" :=
+  (\big[+%N/0%N]_(i | P%B) F%N) : nat_scope.
+Notation "\sum_ i F" :=
+  (\big[+%N/0%N]_i F%N) : nat_scope.
+Notation "\sum_ ( i : t | P ) F" :=
+  (\big[+%N/0%N]_(i : t | P%B) F%N) (only parsing) : nat_scope.
+Notation "\sum_ ( i : t ) F" :=
+  (\big[+%N/0%N]_(i : t) F%N) (only parsing) : nat_scope.
+Notation "\sum_ ( i < n | P ) F" :=
+  (\big[+%N/0%N]_(i < n | P%B) F%N) : nat_scope.
+Notation "\sum_ ( i < n ) F" :=
+  (\big[+%N/0%N]_(i < n) F%N) : nat_scope.
+Notation "\sum_ ( i 'in' A | P ) F" :=
+  (\big[+%N/0%N]_(i in A | P%B) F%N) : nat_scope.
+Notation "\sum_ ( i 'in' A ) F" :=
+  (\big[+%N/0%N]_(i in A) F%N) : nat_scope.
+ +
+Notation "\prod_ ( i <- r | P ) F" :=
+  (\big[*%N/1%N]_(i <- r | P%B) F%N) : nat_scope.
+Notation "\prod_ ( i <- r ) F" :=
+  (\big[*%N/1%N]_(i <- r) F%N) : nat_scope.
+Notation "\prod_ ( m <= i < n | P ) F" :=
+  (\big[*%N/1%N]_(m ≤ i < n | P%B) F%N) : nat_scope.
+Notation "\prod_ ( m <= i < n ) F" :=
+  (\big[*%N/1%N]_(m ≤ i < n) F%N) : nat_scope.
+Notation "\prod_ ( i | P ) F" :=
+  (\big[*%N/1%N]_(i | P%B) F%N) : nat_scope.
+Notation "\prod_ i F" :=
+  (\big[*%N/1%N]_i F%N) : nat_scope.
+Notation "\prod_ ( i : t | P ) F" :=
+  (\big[*%N/1%N]_(i : t | P%B) F%N) (only parsing) : nat_scope.
+Notation "\prod_ ( i : t ) F" :=
+  (\big[*%N/1%N]_(i : t) F%N) (only parsing) : nat_scope.
+Notation "\prod_ ( i < n | P ) F" :=
+  (\big[*%N/1%N]_(i < n | P%B) F%N) : nat_scope.
+Notation "\prod_ ( i < n ) F" :=
+  (\big[*%N/1%N]_(i < n) F%N) : nat_scope.
+Notation "\prod_ ( i 'in' A | P ) F" :=
+  (\big[*%N/1%N]_(i in A | P%B) F%N) : nat_scope.
+Notation "\prod_ ( i 'in' A ) F" :=
+  (\big[*%N/1%N]_(i in A) F%N) : nat_scope.
+ +
+Notation "\max_ ( i <- r | P ) F" :=
+  (\big[maxn/0%N]_(i <- r | P%B) F%N) : nat_scope.
+Notation "\max_ ( i <- r ) F" :=
+  (\big[maxn/0%N]_(i <- r) F%N) : nat_scope.
+Notation "\max_ ( i | P ) F" :=
+  (\big[maxn/0%N]_(i | P%B) F%N) : nat_scope.
+Notation "\max_ i F" :=
+  (\big[maxn/0%N]_i F%N) : nat_scope.
+Notation "\max_ ( i : I | P ) F" :=
+  (\big[maxn/0%N]_(i : I | P%B) F%N) (only parsing) : nat_scope.
+Notation "\max_ ( i : I ) F" :=
+  (\big[maxn/0%N]_(i : I) F%N) (only parsing) : nat_scope.
+Notation "\max_ ( m <= i < n | P ) F" :=
+ (\big[maxn/0%N]_(m ≤ i < n | P%B) F%N) : nat_scope.
+Notation "\max_ ( m <= i < n ) F" :=
+ (\big[maxn/0%N]_(m ≤ i < n) F%N) : nat_scope.
+Notation "\max_ ( i < n | P ) F" :=
+ (\big[maxn/0%N]_(i < n | P%B) F%N) : nat_scope.
+Notation "\max_ ( i < n ) F" :=
+ (\big[maxn/0%N]_(i < n) F%N) : nat_scope.
+Notation "\max_ ( i 'in' A | P ) F" :=
+ (\big[maxn/0%N]_(i in A | P%B) F%N) : nat_scope.
+Notation "\max_ ( i 'in' A ) F" :=
+ (\big[maxn/0%N]_(i in A) F%N) : nat_scope.

@@ -778,9 +777,9 @@ Print Canonical Projections. Induction loading
-Lemma big_load R (K K' : R → Type) idx op I r (P : pred I) F :
-  K (\big[op/idx]_(i <- r | P i) F i) × K' (\big[op/idx]_(i <- r | P i) F i)
-  → K' (\big[op/idx]_(i <- r | P i) F i).
+Lemma big_load R (K K' : R → Type) idx op I r (P : pred I) F :
+  K (\big[op/idx]_(i <- r | P i) F i) × K' (\big[op/idx]_(i <- r | P i) F i)
+  → K' (\big[op/idx]_(i <- r | P i) F i).

@@ -788,30 +787,30 @@ Print Canonical Projections. Section Elim3.

-Variables (R1 R2 R3 : Type) (K : R1 → R2 → R3 → Type).
-Variables (id1 : R1) (op1 : R1 → R1 → R1).
-Variables (id2 : R2) (op2 : R2 → R2 → R2).
-Variables (id3 : R3) (op3 : R3 → R3 → R3).
+Variables (R1 R2 R3 : Type) (K : R1 → R2 → R3 → Type).
+Variables (id1 : R1) (op1 : R1 → R1 → R1).
+Variables (id2 : R2) (op2 : R2 → R2 → R2).
+Variables (id3 : R3) (op3 : R3 → R3 → R3).

Hypothesis Kid : K id1 id2 id3.

-Lemma big_rec3 I r (P : pred I) F1 F2 F3
-    (K_F : ∀ i y1 y2 y3, P i → K y1 y2 y3 →
+Lemma big_rec3 I r (P : pred I) F1 F2 F3
+    (K_F : ∀ i y1 y2 y3, P i → K y1 y2 y3 →
       K (op1 (F1 i) y1) (op2 (F2 i) y2) (op3 (F3 i) y3)) :
-  K (\big[op1/id1]_(i <- r | P i) F1 i)
-    (\big[op2/id2]_(i <- r | P i) F2 i)
-    (\big[op3/id3]_(i <- r | P i) F3 i).
+  K (\big[op1/id1]_(i <- r | P i) F1 i)
+    (\big[op2/id2]_(i <- r | P i) F2 i)
+    (\big[op3/id3]_(i <- r | P i) F3 i).

Hypothesis Kop : ∀ x1 x2 x3 y1 y2 y3,
-  K x1 x2 x3 → K y1 y2 y3→ K (op1 x1 y1) (op2 x2 y2) (op3 x3 y3).
-Lemma big_ind3 I r (P : pred I) F1 F2 F3
-   (K_F : ∀ i, P i → K (F1 i) (F2 i) (F3 i)) :
-  K (\big[op1/id1]_(i <- r | P i) F1 i)
-    (\big[op2/id2]_(i <- r | P i) F2 i)
-    (\big[op3/id3]_(i <- r | P i) F3 i).
+  K x1 x2 x3 → K y1 y2 y3→ K (op1 x1 y1) (op2 x2 y2) (op3 x3 y3).
+Lemma big_ind3 I r (P : pred I) F1 F2 F3
+   (K_F : ∀ i, P i → K (F1 i) (F2 i) (F3 i)) :
+  K (\big[op1/id1]_(i <- r | P i) F1 i)
+    (\big[op2/id2]_(i <- r | P i) F2 i)
+    (\big[op3/id3]_(i <- r | P i) F3 i).

End Elim3.
@@ -822,29 +821,29 @@ Print Canonical Projections. Section Elim2.

-Variables (R1 R2 : Type) (K : R1 → R2 → Type) (f : R2 → R1).
-Variables (id1 : R1) (op1 : R1 → R1 → R1).
-Variables (id2 : R2) (op2 : R2 → R2 → R2).
+Variables (R1 R2 : Type) (K : R1 → R2 → Type) (f : R2 → R1).
+Variables (id1 : R1) (op1 : R1 → R1 → R1).
+Variables (id2 : R2) (op2 : R2 → R2 → R2).

Hypothesis Kid : K id1 id2.

-Lemma big_rec2 I r (P : pred I) F1 F2
-    (K_F : ∀ i y1 y2, P i → K y1 y2 →
+Lemma big_rec2 I r (P : pred I) F1 F2
+    (K_F : ∀ i y1 y2, P i → K y1 y2 →
       K (op1 (F1 i) y1) (op2 (F2 i) y2)) :
-  K (\big[op1/id1]_(i <- r | P i) F1 i) (\big[op2/id2]_(i <- r | P i) F2 i).
+  K (\big[op1/id1]_(i <- r | P i) F1 i) (\big[op2/id2]_(i <- r | P i) F2 i).

Hypothesis Kop : ∀ x1 x2 y1 y2,
-  K x1 x2 → K y1 y2 → K (op1 x1 y1) (op2 x2 y2).
-Lemma big_ind2 I r (P : pred I) F1 F2 (K_F : ∀ i, P i → K (F1 i) (F2 i)) :
-  K (\big[op1/id1]_(i <- r | P i) F1 i) (\big[op2/id2]_(i <- r | P i) F2 i).
+  K x1 x2 → K y1 y2 → K (op1 x1 y1) (op2 x2 y2).
+Lemma big_ind2 I r (P : pred I) F1 F2 (K_F : ∀ i, P i → K (F1 i) (F2 i)) :
+  K (\big[op1/id1]_(i <- r | P i) F1 i) (\big[op2/id2]_(i <- r | P i) F2 i).

-Hypotheses (f_op : {morph f : x y / op2 x y >-> op1 x y}) (f_id : f id2 = id1).
-Lemma big_morph I r (P : pred I) F :
-  f (\big[op2/id2]_(i <- r | P i) F i) = \big[op1/id1]_(i <- r | P i) f (F i).
+Hypotheses (f_op : {morph f : x y / op2 x y >-> op1 x y}) (f_id : f id2 = id1).
+Lemma big_morph I r (P : pred I) F :
+  f (\big[op2/id2]_(i <- r | P i) F i) = \big[op1/id1]_(i <- r | P i) f (F i).

End Elim2.
@@ -855,31 +854,31 @@ Print Canonical Projections. Section Elim1.

-Variables (R : Type) (K : R → Type) (f : R → R).
-Variables (idx : R) (op op' : R → R → R).
+Variables (R : Type) (K : R → Type) (f : R → R).
+Variables (idx : R) (op op' : R → R → R).

Hypothesis Kid : K idx.

-Lemma big_rec I r (P : pred I) F
-    (Kop : ∀ i x, P i → K x → K (op (F i) x)) :
-  K (\big[op/idx]_(i <- r | P i) F i).
+Lemma big_rec I r (P : pred I) F
+    (Kop : ∀ i x, P i → K x → K (op (F i) x)) :
+  K (\big[op/idx]_(i <- r | P i) F i).

-Hypothesis Kop : ∀ x y, K x → K y → K (op x y).
-Lemma big_ind I r (P : pred I) F (K_F : ∀ i, P i → K (F i)) :
-  K (\big[op/idx]_(i <- r | P i) F i).
+Hypothesis Kop : ∀ x y, K x → K y → K (op x y).
+Lemma big_ind I r (P : pred I) F (K_F : ∀ i, P i → K (F i)) :
+  K (\big[op/idx]_(i <- r | P i) F i).

-Hypothesis Kop' : ∀ x y, K x → K y → op x y = op' x y.
-Lemma eq_big_op I r (P : pred I) F (K_F : ∀ i, P i → K (F i)) :
-  \big[op/idx]_(i <- r | P i) F i = \big[op'/idx]_(i <- r | P i) F i.
+Hypothesis Kop' : ∀ x y, K x → K y → op x y = op' x y.
+Lemma eq_big_op I r (P : pred I) F (K_F : ∀ i, P i → K (F i)) :
+  \big[op/idx]_(i <- r | P i) F i = \big[op'/idx]_(i <- r | P i) F i.

-Hypotheses (fM : {morph f : x y / op x y}) (f_id : f idx = idx).
-Lemma big_endo I r (P : pred I) F :
-  f (\big[op/idx]_(i <- r | P i) F i) = \big[op/idx]_(i <- r | P i) f (F i).
+Hypotheses (fM : {morph f : x y / op x y}) (f_id : f idx = idx).
+Lemma big_endo I r (P : pred I) F :
+  f (\big[op/idx]_(i <- r | P i) F i) = \big[op/idx]_(i <- r | P i) f (F i).

End Elim1.
@@ -890,7 +889,7 @@ Print Canonical Projections. Section Extensionality.

-Variables (R : Type) (idx : R) (op : R → R → R).
+Variables (R : Type) (idx : R) (op : R → R → R).

Section SeqExtension.
@@ -899,18 +898,21 @@ Print Canonical Projections. Variable I : Type.

-Lemma big_filter r (P : pred I) F :
-  \big[op/idx]_(i <- filter P r) F i = \big[op/idx]_(i <- r | P i) F i.
+Lemma foldrE r : foldr op idx r = \big[op/idx]_(x <- r) x.

-Lemma big_filter_cond r (P1 P2 : pred I) F :
-  \big[op/idx]_(i <- filter P1 r | P2 i) F i
-     = \big[op/idx]_(i <- r | P1 i && P2 i) F i.
+Lemma big_filter r (P : pred I) F :
+  \big[op/idx]_(i <- filter P r) F i = \big[op/idx]_(i <- r | P i) F i.
+ +
+Lemma big_filter_cond r (P1 P2 : pred I) F :
+  \big[op/idx]_(i <- filter P1 r | P2 i) F i
+     = \big[op/idx]_(i <- r | P1 i && P2 i) F i.

-Lemma eq_bigl r (P1 P2 : pred I) F :
-    P1 =1 P2 →
-  \big[op/idx]_(i <- r | P1 i) F i = \big[op/idx]_(i <- r | P2 i) F i.
+Lemma eq_bigl r (P1 P2 : pred I) F :
+    P1 =1 P2 →
+  \big[op/idx]_(i <- r | P1 i) F i = \big[op/idx]_(i <- r | P2 i) F i.

@@ -919,75 +921,80 @@ Print Canonical Projections. A lemma to permute aggregate conditions.
-Lemma big_andbC r (P Q : pred I) F :
-  \big[op/idx]_(i <- r | P i && Q i) F i
-    = \big[op/idx]_(i <- r | Q i && P i) F i.
+Lemma big_andbC r (P Q : pred I) F :
+  \big[op/idx]_(i <- r | P i && Q i) F i
+    = \big[op/idx]_(i <- r | Q i && P i) F i.

-Lemma eq_bigr r (P : pred I) F1 F2 : (∀ i, P i → F1 i = F2 i) →
-  \big[op/idx]_(i <- r | P i) F1 i = \big[op/idx]_(i <- r | P i) F2 i.
+Lemma eq_bigr r (P : pred I) F1 F2 : (∀ i, P i → F1 i = F2 i) →
+  \big[op/idx]_(i <- r | P i) F1 i = \big[op/idx]_(i <- r | P i) F2 i.

-Lemma eq_big r (P1 P2 : pred I) F1 F2 :
-    P1 =1 P2 → (∀ i, P1 i → F1 i = F2 i) →
-  \big[op/idx]_(i <- r | P1 i) F1 i = \big[op/idx]_(i <- r | P2 i) F2 i.
+Lemma eq_big r (P1 P2 : pred I) F1 F2 :
+    P1 =1 P2 → (∀ i, P1 i → F1 i = F2 i) →
+  \big[op/idx]_(i <- r | P1 i) F1 i = \big[op/idx]_(i <- r | P2 i) F2 i.

-Lemma congr_big r1 r2 (P1 P2 : pred I) F1 F2 :
-    r1 = r2 → P1 =1 P2 → (∀ i, P1 i → F1 i = F2 i) →
-  \big[op/idx]_(i <- r1 | P1 i) F1 i = \big[op/idx]_(i <- r2 | P2 i) F2 i.
+Lemma congr_big r1 r2 (P1 P2 : pred I) F1 F2 :
+    r1 = r2 → P1 =1 P2 → (∀ i, P1 i → F1 i = F2 i) →
+  \big[op/idx]_(i <- r1 | P1 i) F1 i = \big[op/idx]_(i <- r2 | P2 i) F2 i.

-Lemma big_nil (P : pred I) F : \big[op/idx]_(i <- [::] | P i) F i = idx.
+Lemma big_nil (P : pred I) F : \big[op/idx]_(i <- [::] | P i) F i = idx.

-Lemma big_cons i r (P : pred I) F :
-    let x := \big[op/idx]_(j <- r | P j) F j in
-  \big[op/idx]_(j <- i :: r | P j) F j = if P i then op (F i) x else x.
+Lemma big_cons i r (P : pred I) F :
+    let x := \big[op/idx]_(j <- r | P j) F j in
+  \big[op/idx]_(j <- i :: r | P j) F j = if P i then op (F i) x else x.

-Lemma big_map J (h : J → I) r (P : pred I) F :
-  \big[op/idx]_(i <- map h r | P i) F i
-     = \big[op/idx]_(j <- r | P (h j)) F (h j).
+Lemma big_map J (h : J → I) r (P : pred I) F :
+  \big[op/idx]_(i <- map h r | P i) F i
+     = \big[op/idx]_(j <- r | P (h j)) F (h j).

-Lemma big_nth x0 r (P : pred I) F :
-  \big[op/idx]_(i <- r | P i) F i
-     = \big[op/idx]_(0 ≤ i < size r | P (nth x0 r i)) (F (nth x0 r i)).
+Lemma big_nth x0 r (P : pred I) F :
+  \big[op/idx]_(i <- r | P i) F i
+     = \big[op/idx]_(0 ≤ i < size r | P (nth x0 r i)) (F (nth x0 r i)).

-Lemma big_hasC r (P : pred I) F :
-  ~~ has P r → \big[op/idx]_(i <- r | P i) F i = idx.
+Lemma big_hasC r (P : pred I) F :
+  ~~ has P r → \big[op/idx]_(i <- r | P i) F i = idx.

-Lemma big_pred0_eq (r : seq I) F : \big[op/idx]_(i <- r | false) F i = idx.
+Lemma big_pred0_eq (r : seq I) F : \big[op/idx]_(i <- r | false) F i = idx.

-Lemma big_pred0 r (P : pred I) F :
-  P =1 xpred0 → \big[op/idx]_(i <- r | P i) F i = idx.
+Lemma big_pred0 r (P : pred I) F :
+  P =1 xpred0 → \big[op/idx]_(i <- r | P i) F i = idx.

-Lemma big_cat_nested r1 r2 (P : pred I) F :
-    let x := \big[op/idx]_(i <- r2 | P i) F i in
-  \big[op/idx]_(i <- r1 ++ r2 | P i) F i = \big[op/x]_(i <- r1 | P i) F i.
+Lemma big_cat_nested r1 r2 (P : pred I) F :
+    let x := \big[op/idx]_(i <- r2 | P i) F i in
+  \big[op/idx]_(i <- r1 ++ r2 | P i) F i = \big[op/x]_(i <- r1 | P i) F i.

-Lemma big_catl r1 r2 (P : pred I) F :
-    ~~ has P r2 →
-  \big[op/idx]_(i <- r1 ++ r2 | P i) F i = \big[op/idx]_(i <- r1 | P i) F i.
+Lemma big_catl r1 r2 (P : pred I) F :
+    ~~ has P r2 →
+  \big[op/idx]_(i <- r1 ++ r2 | P i) F i = \big[op/idx]_(i <- r1 | P i) F i.

-Lemma big_catr r1 r2 (P : pred I) F :
-     ~~ has P r1 →
-  \big[op/idx]_(i <- r1 ++ r2 | P i) F i = \big[op/idx]_(i <- r2 | P i) F i.
+Lemma big_catr r1 r2 (P : pred I) F :
+     ~~ has P r1 →
+  \big[op/idx]_(i <- r1 ++ r2 | P i) F i = \big[op/idx]_(i <- r2 | P i) F i.

-Lemma big_const_seq r (P : pred I) x :
-  \big[op/idx]_(i <- r | P i) x = iter (count P r) (op x) idx.
+Lemma big_const_seq r (P : pred I) x :
+  \big[op/idx]_(i <- r | P i) x = iter (count P r) (op x) idx.

End SeqExtension.
+
+Lemma big_map_id J (h : J → R) r (P : pred R) :
+  \big[op/idx]_(i <- map h r | P i) i
+     = \big[op/idx]_(j <- r | P (h j)) h j.
+
@@ -997,17 +1004,17 @@ Print Canonical Projections. congruence or induction lemmas.
-Lemma big_seq_cond (I : eqType) r (P : pred I) F :
-  \big[op/idx]_(i <- r | P i) F i
-    = \big[op/idx]_(i <- r | (i \in r) && P i) F i.
+Lemma big_seq_cond (I : eqType) r (P : pred I) F :
+  \big[op/idx]_(i <- r | P i) F i
+    = \big[op/idx]_(i <- r | (i \in r) && P i) F i.

Lemma big_seq (I : eqType) (r : seq I) F :
-  \big[op/idx]_(i <- r) F i = \big[op/idx]_(i <- r | i \in r) F i.
+  \big[op/idx]_(i <- r) F i = \big[op/idx]_(i <- r | i \in r) F i.

Lemma eq_big_seq (I : eqType) (r : seq I) F1 F2 :
-  {in r, F1 =1 F2} → \big[op/idx]_(i <- r) F1 i = \big[op/idx]_(i <- r) F2 i.
+  {in r, F1 =1 F2} → \big[op/idx]_(i <- r) F1 i = \big[op/idx]_(i <- r) F2 i.

@@ -1016,148 +1023,166 @@ Print Canonical Projections. Similar lemmas for exposing integer indexing in the predicate.
-Lemma big_nat_cond m n (P : pred nat) F :
-  \big[op/idx]_(m ≤ i < n | P i) F i
-    = \big[op/idx]_(m ≤ i < n | (m ≤ i < n) && P i) F i.
+Lemma big_nat_cond m n (P : pred nat) F :
+  \big[op/idx]_(m ≤ i < n | P i) F i
+    = \big[op/idx]_(m ≤ i < n | (m ≤ i < n) && P i) F i.

Lemma big_nat m n F :
-  \big[op/idx]_(m ≤ i < n) F i = \big[op/idx]_(m ≤ i < n | m ≤ i < n) F i.
+  \big[op/idx]_(m ≤ i < n) F i = \big[op/idx]_(m ≤ i < n | m ≤ i < n) F i.

Lemma congr_big_nat m1 n1 m2 n2 P1 P2 F1 F2 :
-    m1 = m2 → n1 = n2 →
-    (∀ i, m1 ≤ i < n2 → P1 i = P2 i) →
-    (∀ i, P1 i && (m1 ≤ i < n2) → F1 i = F2 i) →
-  \big[op/idx]_(m1 ≤ i < n1 | P1 i) F1 i
-    = \big[op/idx]_(m2 ≤ i < n2 | P2 i) F2 i.
+    m1 = m2 → n1 = n2 →
+    (∀ i, m1 ≤ i < n2 → P1 i = P2 i) →
+    (∀ i, P1 i && (m1 ≤ i < n2) → F1 i = F2 i) →
+  \big[op/idx]_(m1 ≤ i < n1 | P1 i) F1 i
+    = \big[op/idx]_(m2 ≤ i < n2 | P2 i) F2 i.

Lemma eq_big_nat m n F1 F2 :
-    (∀ i, m ≤ i < n → F1 i = F2 i) →
-  \big[op/idx]_(m ≤ i < n) F1 i = \big[op/idx]_(m ≤ i < n) F2 i.
+    (∀ i, m ≤ i < n → F1 i = F2 i) →
+  \big[op/idx]_(m ≤ i < n) F1 i = \big[op/idx]_(m ≤ i < n) F2 i.

-Lemma big_geq m n (P : pred nat) F :
-  m ≥ n → \big[op/idx]_(m ≤ i < n | P i) F i = idx.
+Lemma big_geq m n (P : pred nat) F :
+  m ≥ n → \big[op/idx]_(m ≤ i < n | P i) F i = idx.

-Lemma big_ltn_cond m n (P : pred nat) F :
-    m < n → let x := \big[op/idx]_(m.+1 ≤ i < n | P i) F i in
-  \big[op/idx]_(m ≤ i < n | P i) F i = if P m then op (F m) x else x.
+Lemma big_ltn_cond m n (P : pred nat) F :
+    m < n → let x := \big[op/idx]_(m.+1 ≤ i < n | P i) F i in
+  \big[op/idx]_(m ≤ i < n | P i) F i = if P m then op (F m) x else x.

Lemma big_ltn m n F :
-     m < n →
-  \big[op/idx]_(m ≤ i < n) F i = op (F m) (\big[op/idx]_(m.+1 ≤ i < n) F i).
+     m < n →
+  \big[op/idx]_(m ≤ i < n) F i = op (F m) (\big[op/idx]_(m.+1 ≤ i < n) F i).

-Lemma big_addn m n a (P : pred nat) F :
-  \big[op/idx]_(m + a ≤ i < n | P i) F i =
-     \big[op/idx]_(m ≤ i < n - a | P (i + a)) F (i + a).
+Lemma big_addn m n a (P : pred nat) F :
+  \big[op/idx]_(m + a ≤ i < n | P i) F i =
+     \big[op/idx]_(m ≤ i < n - a | P (i + a)) F (i + a).

-Lemma big_add1 m n (P : pred nat) F :
-  \big[op/idx]_(m.+1 ≤ i < n | P i) F i =
-     \big[op/idx]_(m ≤ i < n.-1 | P (i.+1)) F (i.+1).
+Lemma big_add1 m n (P : pred nat) F :
+  \big[op/idx]_(m.+1 ≤ i < n | P i) F i =
+     \big[op/idx]_(m ≤ i < n.-1 | P (i.+1)) F (i.+1).

-Lemma big_nat_recl n m F : m ≤ n →
-  \big[op/idx]_(m ≤ i < n.+1) F i =
-     op (F m) (\big[op/idx]_(m ≤ i < n) F i.+1).
+Lemma big_nat_recl n m F : m ≤ n →
+  \big[op/idx]_(m ≤ i < n.+1) F i =
+     op (F m) (\big[op/idx]_(m ≤ i < n) F i.+1).

-Lemma big_mkord n (P : pred nat) F :
-  \big[op/idx]_(0 ≤ i < n | P i) F i = \big[op/idx]_(i < n | P i) F i.
+Lemma big_mkord n (P : pred nat) F :
+  \big[op/idx]_(0 ≤ i < n | P i) F i = \big[op/idx]_(i < n | P i) F i.

-Lemma big_nat_widen m n1 n2 (P : pred nat) F :
-     n1 ≤ n2 →
-  \big[op/idx]_(m ≤ i < n1 | P i) F i
-      = \big[op/idx]_(m ≤ i < n2 | P i && (i < n1)) F i.
+Lemma big_nat_widen m n1 n2 (P : pred nat) F :
+     n1 ≤ n2 →
+  \big[op/idx]_(m ≤ i < n1 | P i) F i
+      = \big[op/idx]_(m ≤ i < n2 | P i && (i < n1)) F i.

-Lemma big_ord_widen_cond n1 n2 (P : pred nat) (F : nat → R) :
-     n1 ≤ n2 →
-  \big[op/idx]_(i < n1 | P i) F i
-      = \big[op/idx]_(i < n2 | P i && (i < n1)) F i.
+Lemma big_ord_widen_cond n1 n2 (P : pred nat) (F : nat → R) :
+     n1 ≤ n2 →
+  \big[op/idx]_(i < n1 | P i) F i
+      = \big[op/idx]_(i < n2 | P i && (i < n1)) F i.

-Lemma big_ord_widen n1 n2 (F : nat → R) :
-    n1 ≤ n2 →
-  \big[op/idx]_(i < n1) F i = \big[op/idx]_(i < n2 | i < n1) F i.
+Lemma big_ord_widen n1 n2 (F : nat → R) :
+    n1 ≤ n2 →
+  \big[op/idx]_(i < n1) F i = \big[op/idx]_(i < n2 | i < n1) F i.

-Lemma big_ord_widen_leq n1 n2 (P : pred 'I_(n1.+1)) F :
-    n1 < n2 →
-  \big[op/idx]_(i < n1.+1 | P i) F i
-      = \big[op/idx]_(i < n2 | P (inord i) && (i ≤ n1)) F (inord i).
+Lemma big_ord_widen_leq n1 n2 (P : pred 'I_(n1.+1)) F :
+    n1 < n2 →
+  \big[op/idx]_(i < n1.+1 | P i) F i
+      = \big[op/idx]_(i < n2 | P (inord i) && (i ≤ n1)) F (inord i).

-Lemma big_ord0 P F : \big[op/idx]_(i < 0 | P i) F i = idx.
+Lemma big_ord0 P F : \big[op/idx]_(i < 0 | P i) F i = idx.

-Lemma big_tnth I r (P : pred I) F :
+Lemma big_tnth I r (P : pred I) F :
  let r_ := tnth (in_tuple r) in
-  \big[op/idx]_(i <- r | P i) F i
-     = \big[op/idx]_(i < size r | P (r_ i)) (F (r_ i)).
+  \big[op/idx]_(i <- r | P i) F i
+     = \big[op/idx]_(i < size r | P (r_ i)) (F (r_ i)).

-Lemma big_index_uniq (I : eqType) (r : seq I) (E : 'I_(size r) → R) :
-    uniq r →
-  \big[op/idx]_i E i = \big[op/idx]_(x <- r) oapp E idx (insub (index x r)).
+Lemma big_index_uniq (I : eqType) (r : seq I) (E : 'I_(size r) → R) :
+    uniq r →
+  \big[op/idx]_i E i = \big[op/idx]_(x <- r) oapp E idx (insub (index x r)).

-Lemma big_tuple I n (t : n.-tuple I) (P : pred I) F :
-  \big[op/idx]_(i <- t | P i) F i
-     = \big[op/idx]_(i < n | P (tnth t i)) F (tnth t i).
+Lemma big_tuple I n (t : n.-tuple I) (P : pred I) F :
+  \big[op/idx]_(i <- t | P i) F i
+     = \big[op/idx]_(i < n | P (tnth t i)) F (tnth t i).

-Lemma big_ord_narrow_cond n1 n2 (P : pred 'I_n2) F (le_n12 : n1 ≤ n2) :
+Lemma big_ord_narrow_cond n1 n2 (P : pred 'I_n2) F (le_n12 : n1 ≤ n2) :
    let w := widen_ord le_n12 in
-  \big[op/idx]_(i < n2 | P i && (i < n1)) F i
-    = \big[op/idx]_(i < n1 | P (w i)) F (w i).
+  \big[op/idx]_(i < n2 | P i && (i < n1)) F i
+    = \big[op/idx]_(i < n1 | P (w i)) F (w i).

-Lemma big_ord_narrow_cond_leq n1 n2 (P : pred _) F (le_n12 : n1 ≤ n2) :
-    let w := @widen_ord n1.+1 n2.+1 le_n12 in
-  \big[op/idx]_(i < n2.+1 | P i && (i ≤ n1)) F i
-  = \big[op/idx]_(i < n1.+1 | P (w i)) F (w i).
+Lemma big_ord_narrow_cond_leq n1 n2 (P : pred _) F (le_n12 : n1 ≤ n2) :
+    let w := @widen_ord n1.+1 n2.+1 le_n12 in
+  \big[op/idx]_(i < n2.+1 | P i && (i ≤ n1)) F i
+  = \big[op/idx]_(i < n1.+1 | P (w i)) F (w i).

-Lemma big_ord_narrow n1 n2 F (le_n12 : n1 ≤ n2) :
+Lemma big_ord_narrow n1 n2 F (le_n12 : n1 ≤ n2) :
    let w := widen_ord le_n12 in
-  \big[op/idx]_(i < n2 | i < n1) F i = \big[op/idx]_(i < n1) F (w i).
+  \big[op/idx]_(i < n2 | i < n1) F i = \big[op/idx]_(i < n1) F (w i).

-Lemma big_ord_narrow_leq n1 n2 F (le_n12 : n1 ≤ n2) :
-    let w := @widen_ord n1.+1 n2.+1 le_n12 in
-  \big[op/idx]_(i < n2.+1 | i ≤ n1) F i = \big[op/idx]_(i < n1.+1) F (w i).
+Lemma big_ord_narrow_leq n1 n2 F (le_n12 : n1 ≤ n2) :
+    let w := @widen_ord n1.+1 n2.+1 le_n12 in
+  \big[op/idx]_(i < n2.+1 | i ≤ n1) F i = \big[op/idx]_(i < n1.+1) F (w i).

Lemma big_ord_recl n F :
-  \big[op/idx]_(i < n.+1) F i =
-     op (F ord0) (\big[op/idx]_(i < n) F (@lift n.+1 ord0 i)).
+  \big[op/idx]_(i < n.+1) F i =
+     op (F ord0) (\big[op/idx]_(i < n) F (@lift n.+1 ord0 i)).

-Lemma big_const (I : finType) (A : pred I) x :
-  \big[op/idx]_(i in A) x = iter #|A| (op x) idx.
+Lemma big_const (I : finType) (A : pred I) x :
+  \big[op/idx]_(i in A) x = iter #|A| (op x) idx.

Lemma big_const_nat m n x :
-  \big[op/idx]_(m ≤ i < n) x = iter (n - m) (op x) idx.
+  \big[op/idx]_(m ≤ i < n) x = iter (n - m) (op x) idx.

Lemma big_const_ord n x :
-  \big[op/idx]_(i < n) x = iter n (op x) idx.
+  \big[op/idx]_(i < n) x = iter n (op x) idx.
+ +
+Lemma big_nseq_cond I n a (P : pred I) F :
+  \big[op/idx]_(i <- nseq n a | P i) F i = if P a then iter n (op (F a)) idx else idx.
+ +
+Lemma big_nseq I n a (F : I → R):
+  \big[op/idx]_(i <- nseq n a) F i = iter n (op (F a)) idx.
+ +
+Lemma big_image_cond I (J : finType) (h : J → I) (A : pred J) (P : pred I) F :
+  \big[op/idx]_(i <- [seq h j | j in A] | P i) F i
+     = \big[op/idx]_(j in A | P (h j)) F (h j).
+ +
+Lemma big_image I (J : finType) (h : J → I) (A : pred J) F :
+  \big[op/idx]_(i <- [seq h j | j in A]) F i = \big[op/idx]_(j in A) F (h j).

-Lemma big_nseq_cond I n a (P : pred I) F :
-  \big[op/idx]_(i <- nseq n a | P i) F i = if P a then iter n (op (F a)) idx else idx.
+Lemma big_image_cond_id (J : finType) (h : J → R) (A : pred J) (P : pred R) :
+  \big[op/idx]_(i <- [seq h j | j in A] | P i) i
+     = \big[op/idx]_(j in A | P (h j)) h j.

-Lemma big_nseq I n a (F : I → R):
-  \big[op/idx]_(i <- nseq n a) F i = iter n (op (F a)) idx.
+Lemma big_image_id (J : finType) (h : J → R) (A : pred J) :
+  \big[op/idx]_(i <- [seq h j | j in A]) i = \big[op/idx]_(j in A) h j.

End Extensionality.
@@ -1183,96 +1208,108 @@ Print Canonical Projections.

-Lemma eq_big_idx_seq idx' I r (P : pred I) F :
-     right_id idx' *%M → has P r →
-   \big[*%M/idx']_(i <- r | P i) F i =\big[*%M/1]_(i <- r | P i) F i.
+Lemma foldlE x r : foldl *%M x r = \big[*%M/1]_(y <- x :: r) y.

-Lemma eq_big_idx idx' (I : finType) i0 (P : pred I) F :
-     P i0 → right_id idx' *%M →
-  \big[*%M/idx']_(i | P i) F i =\big[*%M/1]_(i | P i) F i.
+Lemma foldl_idx r : foldl *%M 1 r = \big[*%M/1]_(x <- r) x.
+ +
+Lemma eq_big_idx_seq idx' I r (P : pred I) F :
+     right_id idx' *%M → has P r →
+   \big[*%M/idx']_(i <- r | P i) F i =\big[*%M/1]_(i <- r | P i) F i.
+ +
+Lemma eq_big_idx idx' (I : finType) i0 (P : pred I) F :
+     P i0 → right_id idx' *%M →
+  \big[*%M/idx']_(i | P i) F i =\big[*%M/1]_(i | P i) F i.

-Lemma big1_eq I r (P : pred I) : \big[*%M/1]_(i <- r | P i) 1 = 1.
+Lemma big1_eq I r (P : pred I) : \big[*%M/1]_(i <- r | P i) 1 = 1.

-Lemma big1 I r (P : pred I) F :
-  (∀ i, P i → F i = 1) → \big[*%M/1]_(i <- r | P i) F i = 1.
+Lemma big1 I r (P : pred I) F :
+  (∀ i, P i → F i = 1) → \big[*%M/1]_(i <- r | P i) F i = 1.

-Lemma big1_seq (I : eqType) r (P : pred I) F :
-    (∀ i, P i && (i \in r) → F i = 1) →
-  \big[*%M/1]_(i <- r | P i) F i = 1.
+Lemma big1_seq (I : eqType) r (P : pred I) F :
+    (∀ i, P i && (i \in r) → F i = 1) →
+  \big[*%M/1]_(i <- r | P i) F i = 1.

-Lemma big_seq1 I (i : I) F : \big[*%M/1]_(j <- [:: i]) F j = F i.
+Lemma big_seq1 I (i : I) F : \big[*%M/1]_(j <- [:: i]) F j = F i.

-Lemma big_mkcond I r (P : pred I) F :
-  \big[*%M/1]_(i <- r | P i) F i =
-     \big[*%M/1]_(i <- r) (if P i then F i else 1).
+Lemma big_mkcond I r (P : pred I) F :
+  \big[*%M/1]_(i <- r | P i) F i =
+     \big[*%M/1]_(i <- r) (if P i then F i else 1).

-Lemma big_mkcondr I r (P Q : pred I) F :
-  \big[*%M/1]_(i <- r | P i && Q i) F i =
-     \big[*%M/1]_(i <- r | P i) (if Q i then F i else 1).
+Lemma big_mkcondr I r (P Q : pred I) F :
+  \big[*%M/1]_(i <- r | P i && Q i) F i =
+     \big[*%M/1]_(i <- r | P i) (if Q i then F i else 1).

-Lemma big_mkcondl I r (P Q : pred I) F :
-  \big[*%M/1]_(i <- r | P i && Q i) F i =
-     \big[*%M/1]_(i <- r | Q i) (if P i then F i else 1).
+Lemma big_mkcondl I r (P Q : pred I) F :
+  \big[*%M/1]_(i <- r | P i && Q i) F i =
+     \big[*%M/1]_(i <- r | Q i) (if P i then F i else 1).

-Lemma big_cat I r1 r2 (P : pred I) F :
-  \big[*%M/1]_(i <- r1 ++ r2 | P i) F i =
-     \big[*%M/1]_(i <- r1 | P i) F i × \big[*%M/1]_(i <- r2 | P i) F i.
+Lemma big_cat I r1 r2 (P : pred I) F :
+  \big[*%M/1]_(i <- r1 ++ r2 | P i) F i =
+     \big[*%M/1]_(i <- r1 | P i) F i × \big[*%M/1]_(i <- r2 | P i) F i.

-Lemma big_allpairs I1 I2 (r1 : seq I1) (r2 : seq I2) F :
-  \big[*%M/1]_(i <- [seq (i1, i2) | i1 <- r1, i2 <- r2]) F i =
-    \big[*%M/1]_(i1 <- r1) \big[op/idx]_(i2 <- r2) F (i1, i2).
+Lemma big_allpairs_dep I1 (I2 : I1 → Type) J (h : ∀ i1, I2 i1 → J)
+    (r1 : seq I1) (r2 : ∀ i1, seq (I2 i1)) (F : J → R) :
+  \big[*%M/1]_(i <- [seq h i1 i2 | i1 <- r1, i2 <- r2 i1]) F i =
+    \big[*%M/1]_(i1 <- r1) \big[*%M/1]_(i2 <- r2 i1) F (h i1 i2).
+
+Lemma big_allpairs I1 I2 (r1 : seq I1) (r2 : seq I2) F :
+  \big[*%M/1]_(i <- [seq (i1, i2) | i1 <- r1, i2 <- r2]) F i =
+    \big[*%M/1]_(i1 <- r1) \big[op/idx]_(i2 <- r2) F (i1, i2).
+
Lemma big_pred1_eq (I : finType) (i : I) F :
-  \big[*%M/1]_(j | j == i) F j = F i.
+  \big[*%M/1]_(j | j == i) F j = F i.

-Lemma big_pred1 (I : finType) i (P : pred I) F :
-  P =1 pred1 i → \big[*%M/1]_(j | P j) F j = F i.
+Lemma big_pred1 (I : finType) i (P : pred I) F :
+  P =1 pred1 i → \big[*%M/1]_(j | P j) F j = F i.

-Lemma big_cat_nat n m p (P : pred nat) F : m ≤ n → n ≤ p →
-  \big[*%M/1]_(m ≤ i < p | P i) F i =
-   (\big[*%M/1]_(m ≤ i < n | P i) F i) × (\big[*%M/1]_(n ≤ i < p | P i) F i).
+Lemma big_cat_nat n m p (P : pred nat) F : m ≤ n → n ≤ p →
+  \big[*%M/1]_(m ≤ i < p | P i) F i =
+   (\big[*%M/1]_(m ≤ i < n | P i) F i) × (\big[*%M/1]_(n ≤ i < p | P i) F i).

-Lemma big_nat1 n F : \big[*%M/1]_(n ≤ i < n.+1) F i = F n.
+Lemma big_nat1 n F : \big[*%M/1]_(n ≤ i < n.+1) F i = F n.

-Lemma big_nat_recr n m F : m ≤ n →
-  \big[*%M/1]_(m ≤ i < n.+1) F i = (\big[*%M/1]_(m ≤ i < n) F i) × F n.
+Lemma big_nat_recr n m F : m ≤ n →
+  \big[*%M/1]_(m ≤ i < n.+1) F i = (\big[*%M/1]_(m ≤ i < n) F i) × F n.

Lemma big_ord_recr n F :
-  \big[*%M/1]_(i < n.+1) F i =
-     (\big[*%M/1]_(i < n) F (widen_ord (leqnSn n) i)) × F ord_max.
+  \big[*%M/1]_(i < n.+1) F i =
+     (\big[*%M/1]_(i < n) F (widen_ord (leqnSn n) i)) × F ord_max.

-Lemma big_sumType (I1 I2 : finType) (P : pred (I1 + I2)) F :
-  \big[*%M/1]_(i | P i) F i =
-        (\big[*%M/1]_(i | P (inl _ i)) F (inl _ i))
-      × (\big[*%M/1]_(i | P (inr _ i)) F (inr _ i)).
+Lemma big_sumType (I1 I2 : finType) (P : pred (I1 + I2)) F :
+  \big[*%M/1]_(i | P i) F i =
+        (\big[*%M/1]_(i | P (inl _ i)) F (inl _ i))
+      × (\big[*%M/1]_(i | P (inr _ i)) F (inr _ i)).

-Lemma big_split_ord m n (P : pred 'I_(m + n)) F :
-  \big[*%M/1]_(i | P i) F i =
-        (\big[*%M/1]_(i | P (lshift n i)) F (lshift n i))
-      × (\big[*%M/1]_(i | P (rshift m i)) F (rshift m i)).
+Lemma big_split_ord m n (P : pred 'I_(m + n)) F :
+  \big[*%M/1]_(i | P i) F i =
+        (\big[*%M/1]_(i | P (lshift n i)) F (lshift n i))
+      × (\big[*%M/1]_(i | P (rshift m i)) F (rshift m i)).

-Lemma big_flatten I rr (P : pred I) F :
-  \big[*%M/1]_(i <- flatten rr | P i) F i
-    = \big[*%M/1]_(r <- rr) \big[*%M/1]_(i <- r | P i) F i.
+Lemma big_flatten I rr (P : pred I) F :
+  \big[*%M/1]_(i <- flatten rr | P i) F i
+    = \big[*%M/1]_(r <- rr) \big[*%M/1]_(i <- r | P i) F i.

End Plain.
@@ -1286,132 +1323,132 @@ Print Canonical Projections.

-Lemma eq_big_perm (I : eqType) r1 r2 (P : pred I) F :
-    perm_eq r1 r2 →
-  \big[*%M/1]_(i <- r1 | P i) F i = \big[*%M/1]_(i <- r2 | P i) F i.
+Lemma perm_big (I : eqType) r1 r2 (P : pred I) F :
+    perm_eq r1 r2 →
+  \big[*%M/1]_(i <- r1 | P i) F i = \big[*%M/1]_(i <- r2 | P i) F i.

Lemma big_uniq (I : finType) (r : seq I) F :
-  uniq r → \big[*%M/1]_(i <- r) F i = \big[*%M/1]_(i in r) F i.
+  uniq r → \big[*%M/1]_(i <- r) F i = \big[*%M/1]_(i in r) F i.

-Lemma big_rem (I : eqType) r x (P : pred I) F :
-    x \in r →
-  \big[*%M/1]_(y <- r | P y) F y
-    = (if P x then F x else 1) × \big[*%M/1]_(y <- rem x r | P y) F y.
+Lemma big_rem (I : eqType) r x (P : pred I) F :
+    x \in r →
+  \big[*%M/1]_(y <- r | P y) F y
+    = (if P x then F x else 1) × \big[*%M/1]_(y <- rem x r | P y) F y.

-Lemma big_undup (I : eqType) (r : seq I) (P : pred I) F :
-    idempotent *%M →
-  \big[*%M/1]_(i <- undup r | P i) F i = \big[*%M/1]_(i <- r | P i) F i.
+Lemma big_undup (I : eqType) (r : seq I) (P : pred I) F :
+    idempotent *%M →
+  \big[*%M/1]_(i <- undup r | P i) F i = \big[*%M/1]_(i <- r | P i) F i.

-Lemma eq_big_idem (I : eqType) (r1 r2 : seq I) (P : pred I) F :
-    idempotent *%M → r1 =i r2 →
-  \big[*%M/1]_(i <- r1 | P i) F i = \big[*%M/1]_(i <- r2 | P i) F i.
+Lemma eq_big_idem (I : eqType) (r1 r2 : seq I) (P : pred I) F :
+    idempotent *%M → r1 =i r2 →
+  \big[*%M/1]_(i <- r1 | P i) F i = \big[*%M/1]_(i <- r2 | P i) F i.

-Lemma big_undup_iterop_count (I : eqType) (r : seq I) (P : pred I) F :
-  \big[*%M/1]_(i <- undup r | P i) iterop (count_mem i r) *%M (F i) 1
-    = \big[*%M/1]_(i <- r | P i) F i.
+Lemma big_undup_iterop_count (I : eqType) (r : seq I) (P : pred I) F :
+  \big[*%M/1]_(i <- undup r | P i) iterop (count_mem i r) *%M (F i) 1
+    = \big[*%M/1]_(i <- r | P i) F i.

-Lemma big_split I r (P : pred I) F1 F2 :
-  \big[*%M/1]_(i <- r | P i) (F1 i × F2 i) =
-    \big[*%M/1]_(i <- r | P i) F1 i × \big[*%M/1]_(i <- r | P i) F2 i.
+Lemma big_split I r (P : pred I) F1 F2 :
+  \big[*%M/1]_(i <- r | P i) (F1 i × F2 i) =
+    \big[*%M/1]_(i <- r | P i) F1 i × \big[*%M/1]_(i <- r | P i) F2 i.

-Lemma bigID I r (a P : pred I) F :
-  \big[*%M/1]_(i <- r | P i) F i =
-    \big[*%M/1]_(i <- r | P i && a i) F i ×
-    \big[*%M/1]_(i <- r | P i && ~~ a i) F i.
+Lemma bigID I r (a P : pred I) F :
+  \big[*%M/1]_(i <- r | P i) F i =
+    \big[*%M/1]_(i <- r | P i && a i) F i ×
+    \big[*%M/1]_(i <- r | P i && ~~ a i) F i.

-Lemma bigU (I : finType) (A B : pred I) F :
-    [disjoint A & B] →
-  \big[*%M/1]_(i in [predU A & B]) F i =
-    (\big[*%M/1]_(i in A) F i) × (\big[*%M/1]_(i in B) F i).
+Lemma bigU (I : finType) (A B : pred I) F :
+    [disjoint A & B] →
+  \big[*%M/1]_(i in [predU A & B]) F i =
+    (\big[*%M/1]_(i in A) F i) × (\big[*%M/1]_(i in B) F i).

-Lemma bigD1 (I : finType) j (P : pred I) F :
-  P j → \big[*%M/1]_(i | P i) F i
-    = F j × \big[*%M/1]_(i | P i && (i != j)) F i.
+Lemma bigD1 (I : finType) j (P : pred I) F :
+  P j → \big[*%M/1]_(i | P i) F i
+    = F j × \big[*%M/1]_(i | P i && (i != j)) F i.

-Lemma bigD1_seq (I : eqType) (r : seq I) j F :
-    j \in r → uniq r →
-  \big[*%M/1]_(i <- r) F i = F j × \big[*%M/1]_(i <- r | i != j) F i.
+Lemma bigD1_seq (I : eqType) (r : seq I) j F :
+    j \in r → uniq r →
+  \big[*%M/1]_(i <- r) F i = F j × \big[*%M/1]_(i <- r | i != j) F i.

-Lemma cardD1x (I : finType) (A : pred I) j :
-  A j → #|SimplPred A| = 1 + #|[pred i | A i & i != j]|.
+Lemma cardD1x (I : finType) (A : pred I) j :
+  A j → #|SimplPred A| = 1 + #|[pred i | A i & i != j]|.

-Lemma partition_big (I J : finType) (P : pred I) p (Q : pred J) F :
-    (∀ i, P i → Q (p i)) →
-      \big[*%M/1]_(i | P i) F i =
-         \big[*%M/1]_(j | Q j) \big[*%M/1]_(i | P i && (p i == j)) F i.
+Lemma partition_big (I J : finType) (P : pred I) p (Q : pred J) F :
+    (∀ i, P i → Q (p i)) →
+      \big[*%M/1]_(i | P i) F i =
+         \big[*%M/1]_(j | Q j) \big[*%M/1]_(i | P i && (p i == j)) F i.


-Lemma reindex_onto (I J : finType) (h : J → I) h' (P : pred I) F :
-   (∀ i, P i → h (h' i) = i) →
-  \big[*%M/1]_(i | P i) F i =
-    \big[*%M/1]_(j | P (h j) && (h' (h j) == j)) F (h j).
+Lemma reindex_onto (I J : finType) (h : J → I) h' (P : pred I) F :
+   (∀ i, P i → h (h' i) = i) →
+  \big[*%M/1]_(i | P i) F i =
+    \big[*%M/1]_(j | P (h j) && (h' (h j) == j)) F (h j).

-Lemma reindex (I J : finType) (h : J → I) (P : pred I) F :
-    {on [pred i | P i], bijective h} →
-  \big[*%M/1]_(i | P i) F i = \big[*%M/1]_(j | P (h j)) F (h j).
+Lemma reindex (I J : finType) (h : J → I) (P : pred I) F :
+    {on [pred i | P i], bijective h} →
+  \big[*%M/1]_(i | P i) F i = \big[*%M/1]_(j | P (h j)) F (h j).

-Lemma reindex_inj (I : finType) (h : I → I) (P : pred I) F :
-  injective h → \big[*%M/1]_(i | P i) F i = \big[*%M/1]_(j | P (h j)) F (h j).
+Lemma reindex_inj (I : finType) (h : I → I) (P : pred I) F :
+  injective h → \big[*%M/1]_(i | P i) F i = \big[*%M/1]_(j | P (h j)) F (h j).

Lemma big_nat_rev m n P F :
-  \big[*%M/1]_(m ≤ i < n | P i) F i
-     = \big[*%M/1]_(m ≤ i < n | P (m + n - i.+1)) F (m + n - i.+1).
+  \big[*%M/1]_(m ≤ i < n | P i) F i
+     = \big[*%M/1]_(m ≤ i < n | P (m + n - i.+1)) F (m + n - i.+1).

-Lemma pair_big_dep (I J : finType) (P : pred I) (Q : I → pred J) F :
-  \big[*%M/1]_(i | P i) \big[*%M/1]_(j | Q i j) F i j =
-    \big[*%M/1]_(p | P p.1 && Q p.1 p.2) F p.1 p.2.
+Lemma pair_big_dep (I J : finType) (P : pred I) (Q : I → pred J) F :
+  \big[*%M/1]_(i | P i) \big[*%M/1]_(j | Q i j) F i j =
+    \big[*%M/1]_(p | P p.1 && Q p.1 p.2) F p.1 p.2.

-Lemma pair_big (I J : finType) (P : pred I) (Q : pred J) F :
-  \big[*%M/1]_(i | P i) \big[*%M/1]_(j | Q j) F i j =
-    \big[*%M/1]_(p | P p.1 && Q p.2) F p.1 p.2.
+Lemma pair_big (I J : finType) (P : pred I) (Q : pred J) F :
+  \big[*%M/1]_(i | P i) \big[*%M/1]_(j | Q j) F i j =
+    \big[*%M/1]_(p | P p.1 && Q p.2) F p.1 p.2.

-Lemma pair_bigA (I J : finType) (F : I → J → R) :
-  \big[*%M/1]_i \big[*%M/1]_j F i j = \big[*%M/1]_p F p.1 p.2.
+Lemma pair_bigA (I J : finType) (F : I → J → R) :
+  \big[*%M/1]_i \big[*%M/1]_j F i j = \big[*%M/1]_p F p.1 p.2.

-Lemma exchange_big_dep I J rI rJ (P : pred I) (Q : I → pred J)
-                       (xQ : pred J) F :
-    (∀ i j, P i → Q i j → xQ j) →
-  \big[*%M/1]_(i <- rI | P i) \big[*%M/1]_(j <- rJ | Q i j) F i j =
-    \big[*%M/1]_(j <- rJ | xQ j) \big[*%M/1]_(i <- rI | P i && Q i j) F i j.
+Lemma exchange_big_dep I J rI rJ (P : pred I) (Q : I → pred J)
+                       (xQ : pred J) F :
+    (∀ i j, P i → Q i j → xQ j) →
+  \big[*%M/1]_(i <- rI | P i) \big[*%M/1]_(j <- rJ | Q i j) F i j =
+    \big[*%M/1]_(j <- rJ | xQ j) \big[*%M/1]_(i <- rI | P i && Q i j) F i j.

-Lemma exchange_big I J rI rJ (P : pred I) (Q : pred J) F :
-  \big[*%M/1]_(i <- rI | P i) \big[*%M/1]_(j <- rJ | Q j) F i j =
-    \big[*%M/1]_(j <- rJ | Q j) \big[*%M/1]_(i <- rI | P i) F i j.
+Lemma exchange_big I J rI rJ (P : pred I) (Q : pred J) F :
+  \big[*%M/1]_(i <- rI | P i) \big[*%M/1]_(j <- rJ | Q j) F i j =
+    \big[*%M/1]_(j <- rJ | Q j) \big[*%M/1]_(i <- rI | P i) F i j.

-Lemma exchange_big_dep_nat m1 n1 m2 n2 (P : pred nat) (Q : rel nat)
-                           (xQ : pred nat) F :
-    (∀ i j, m1 ≤ i < n1 → m2 ≤ j < n2 → P i → Q i j → xQ j) →
-  \big[*%M/1]_(m1 ≤ i < n1 | P i) \big[*%M/1]_(m2 ≤ j < n2 | Q i j) F i j =
-    \big[*%M/1]_(m2 ≤ j < n2 | xQ j)
-       \big[*%M/1]_(m1 ≤ i < n1 | P i && Q i j) F i j.
+Lemma exchange_big_dep_nat m1 n1 m2 n2 (P : pred nat) (Q : rel nat)
+                           (xQ : pred nat) F :
+    (∀ i j, m1 ≤ i < n1 → m2 ≤ j < n2 → P i → Q i j → xQ j) →
+  \big[*%M/1]_(m1 ≤ i < n1 | P i) \big[*%M/1]_(m2 ≤ j < n2 | Q i j) F i j =
+    \big[*%M/1]_(m2 ≤ j < n2 | xQ j)
+       \big[*%M/1]_(m1 ≤ i < n1 | P i && Q i j) F i j.

-Lemma exchange_big_nat m1 n1 m2 n2 (P Q : pred nat) F :
-  \big[*%M/1]_(m1 ≤ i < n1 | P i) \big[*%M/1]_(m2 ≤ j < n2 | Q j) F i j =
-    \big[*%M/1]_(m2 ≤ j < n2 | Q j) \big[*%M/1]_(m1 ≤ i < n1 | P i) F i j.
+Lemma exchange_big_nat m1 n1 m2 n2 (P Q : pred nat) F :
+  \big[*%M/1]_(m1 ≤ i < n1 | P i) \big[*%M/1]_(m2 ≤ j < n2 | Q j) F i j =
+    \big[*%M/1]_(m2 ≤ j < n2 | Q j) \big[*%M/1]_(m1 ≤ i < n1 | P i) F i j.

End Abelian.
@@ -1431,45 +1468,45 @@ Print Canonical Projections. Variable R : Type.
Variables zero one : R.
Variable times : Monoid.mul_law 0.
-Variable plus : Monoid.add_law 0 *%M.
+Variable plus : Monoid.add_law 0 *%M.

-Lemma big_distrl I r a (P : pred I) F :
-  \big[+%M/0]_(i <- r | P i) F i × a = \big[+%M/0]_(i <- r | P i) (F i × a).
+Lemma big_distrl I r a (P : pred I) F :
+  \big[+%M/0]_(i <- r | P i) F i × a = \big[+%M/0]_(i <- r | P i) (F i × a).

-Lemma big_distrr I r a (P : pred I) F :
-  a × \big[+%M/0]_(i <- r | P i) F i = \big[+%M/0]_(i <- r | P i) (a × F i).
+Lemma big_distrr I r a (P : pred I) F :
+  a × \big[+%M/0]_(i <- r | P i) F i = \big[+%M/0]_(i <- r | P i) (a × F i).

-Lemma big_distrlr I J rI rJ (pI : pred I) (pJ : pred J) F G :
-  (\big[+%M/0]_(i <- rI | pI i) F i) × (\big[+%M/0]_(j <- rJ | pJ j) G j)
-   = \big[+%M/0]_(i <- rI | pI i) \big[+%M/0]_(j <- rJ | pJ j) (F i × G j).
+Lemma big_distrlr I J rI rJ (pI : pred I) (pJ : pred J) F G :
+  (\big[+%M/0]_(i <- rI | pI i) F i) × (\big[+%M/0]_(j <- rJ | pJ j) G j)
+   = \big[+%M/0]_(i <- rI | pI i) \big[+%M/0]_(j <- rJ | pJ j) (F i × G j).

-Lemma big_distr_big_dep (I J : finType) j0 (P : pred I) (Q : I → pred J) F :
-  \big[*%M/1]_(i | P i) \big[+%M/0]_(j | Q i j) F i j =
-     \big[+%M/0]_(f in pfamily j0 P Q) \big[*%M/1]_(i | P i) F i (f i).
+Lemma big_distr_big_dep (I J : finType) j0 (P : pred I) (Q : I → pred J) F :
+  \big[*%M/1]_(i | P i) \big[+%M/0]_(j | Q i j) F i j =
+     \big[+%M/0]_(f in pfamily j0 P Q) \big[*%M/1]_(i | P i) F i (f i).

-Lemma big_distr_big (I J : finType) j0 (P : pred I) (Q : pred J) F :
-  \big[*%M/1]_(i | P i) \big[+%M/0]_(j | Q j) F i j =
-     \big[+%M/0]_(f in pffun_on j0 P Q) \big[*%M/1]_(i | P i) F i (f i).
+Lemma big_distr_big (I J : finType) j0 (P : pred I) (Q : pred J) F :
+  \big[*%M/1]_(i | P i) \big[+%M/0]_(j | Q j) F i j =
+     \big[+%M/0]_(f in pffun_on j0 P Q) \big[*%M/1]_(i | P i) F i (f i).

-Lemma bigA_distr_big_dep (I J : finType) (Q : I → pred J) F :
-  \big[*%M/1]_i \big[+%M/0]_(j | Q i j) F i j
-    = \big[+%M/0]_(f in family Q) \big[*%M/1]_i F i (f i).
+Lemma bigA_distr_big_dep (I J : finType) (Q : I → pred J) F :
+  \big[*%M/1]_i \big[+%M/0]_(j | Q i j) F i j
+    = \big[+%M/0]_(f in family Q) \big[*%M/1]_i F i (f i).

-Lemma bigA_distr_big (I J : finType) (Q : pred J) (F : I → J → R) :
-  \big[*%M/1]_i \big[+%M/0]_(j | Q j) F i j
-    = \big[+%M/0]_(f in ffun_on Q) \big[*%M/1]_i F i (f i).
+Lemma bigA_distr_big (I J : finType) (Q : pred J) (F : I → J → R) :
+  \big[*%M/1]_i \big[+%M/0]_(j | Q j) F i j
+    = \big[+%M/0]_(f in ffun_on Q) \big[*%M/1]_i F i (f i).

Lemma bigA_distr_bigA (I J : finType) F :
-  \big[*%M/1]_(i : I) \big[+%M/0]_(j : J) F i j
-    = \big[+%M/0]_(f : {ffun I → J}) \big[*%M/1]_i F i (f i).
+  \big[*%M/1]_(i : I) \big[+%M/0]_(j : J) F i j
+    = \big[+%M/0]_(f : {ffun I → J}) \big[*%M/1]_i F i (f i).

End Distributivity.
@@ -1483,20 +1520,20 @@ Print Canonical Projections. Section Seq.

-Variables (I : Type) (r : seq I) (P B : pred I).
+Variables (I : Type) (r : seq I) (P B : pred I).

-Lemma big_has : \big[orb/false]_(i <- r) B i = has B r.
+Lemma big_has : \big[orb/false]_(i <- r) B i = has B r.

-Lemma big_all : \big[andb/true]_(i <- r) B i = all B r.
+Lemma big_all : \big[andb/true]_(i <- r) B i = all B r.

-Lemma big_has_cond : \big[orb/false]_(i <- r | P i) B i = has (predI P B) r.
+Lemma big_has_cond : \big[orb/false]_(i <- r | P i) B i = has (predI P B) r.

Lemma big_all_cond :
-  \big[andb/true]_(i <- r | P i) B i = all [pred i | P i ==> B i] r.
+  \big[andb/true]_(i <- r | P i) B i = all [pred i | P i ==> B i] r.

End Seq.
@@ -1505,13 +1542,13 @@ Print Canonical Projections. Section FinType.

-Variables (I : finType) (P B : pred I).
+Variables (I : finType) (P B : pred I).

-Lemma big_orE : \big[orb/false]_(i | P i) B i = [∃ (i | P i), B i].
+Lemma big_orE : \big[orb/false]_(i | P i) B i = [∃ (i | P i), B i].

-Lemma big_andE : \big[andb/true]_(i | P i) B i = [∀ (i | P i), B i].
+Lemma big_andE : \big[andb/true]_(i | P i) B i = [∀ (i | P i), B i].

End FinType.
@@ -1523,102 +1560,111 @@ Print Canonical Projections. Section NatConst.

-Variables (I : finType) (A : pred I).
+Variables (I : finType) (A : pred I).

-Lemma sum_nat_const n : \sum_(i in A) n = #|A| × n.
+Lemma sum_nat_const n : \sum_(i in A) n = #|A| × n.

-Lemma sum1_card : \sum_(i in A) 1 = #|A|.
+Lemma sum1_card : \sum_(i in A) 1 = #|A|.

-Lemma sum1_count J (r : seq J) (a : pred J) : \sum_(j <- r | a j) 1 = count a r.
+Lemma sum1_count J (r : seq J) (a : pred J) : \sum_(j <- r | a j) 1 = count a r.

-Lemma sum1_size J (r : seq J) : \sum_(j <- r) 1 = size r.
+Lemma sum1_size J (r : seq J) : \sum_(j <- r) 1 = size r.

-Lemma prod_nat_const n : \prod_(i in A) n = n ^ #|A|.
+Lemma prod_nat_const n : \prod_(i in A) n = n ^ #|A|.

-Lemma sum_nat_const_nat n1 n2 n : \sum_(n1 ≤ i < n2) n = (n2 - n1) × n.
+Lemma sum_nat_const_nat n1 n2 n : \sum_(n1 ≤ i < n2) n = (n2 - n1) × n.

-Lemma prod_nat_const_nat n1 n2 n : \prod_(n1 ≤ i < n2) n = n ^ (n2 - n1).
+Lemma prod_nat_const_nat n1 n2 n : \prod_(n1 ≤ i < n2) n = n ^ (n2 - n1).

End NatConst.

-Lemma leqif_sum (I : finType) (P C : pred I) (E1 E2 : I → nat) :
-    (∀ i, P i → E1 i ≤ E2 i ?= iff C i) →
-  \sum_(i | P i) E1 i ≤ \sum_(i | P i) E2 i ?= iff [∀ (i | P i), C i].
+Lemma sumnE r : sumn r = \sum_(i <- r) i.
+ +
+Lemma leqif_sum (I : finType) (P C : pred I) (E1 E2 : I → nat) :
+    (∀ i, P i → E1 i ≤ E2 i ?= iff C i) →
+  \sum_(i | P i) E1 i ≤ \sum_(i | P i) E2 i ?= iff [∀ (i | P i), C i].

-Lemma leq_sum I r (P : pred I) (E1 E2 : I → nat) :
-    (∀ i, P i → E1 i ≤ E2 i) →
-  \sum_(i <- r | P i) E1 i ≤ \sum_(i <- r | P i) E2 i.
+Lemma leq_sum I r (P : pred I) (E1 E2 : I → nat) :
+    (∀ i, P i → E1 i ≤ E2 i) →
+  \sum_(i <- r | P i) E1 i ≤ \sum_(i <- r | P i) E2 i.

-Lemma sum_nat_eq0 (I : finType) (P : pred I) (E : I → nat) :
-  (\sum_(i | P i) E i == 0)%N = [∀ (i | P i), E i == 0%N].
+Lemma sum_nat_eq0 (I : finType) (P : pred I) (E : I → nat) :
+  (\sum_(i | P i) E i == 0)%N = [∀ (i | P i), E i == 0%N].

-Lemma prodn_cond_gt0 I r (P : pred I) F :
-  (∀ i, P i → 0 < F i) → 0 < \prod_(i <- r | P i) F i.
+Lemma prodn_cond_gt0 I r (P : pred I) F :
+  (∀ i, P i → 0 < F i) → 0 < \prod_(i <- r | P i) F i.

-Lemma prodn_gt0 I r (P : pred I) F :
-  (∀ i, 0 < F i) → 0 < \prod_(i <- r | P i) F i.
+Lemma prodn_gt0 I r (P : pred I) F :
+  (∀ i, 0 < F i) → 0 < \prod_(i <- r | P i) F i.

-Lemma leq_bigmax_cond (I : finType) (P : pred I) F i0 :
-  P i0 → F i0 ≤ \max_(i | P i) F i.
+Lemma leq_bigmax_cond (I : finType) (P : pred I) F i0 :
+  P i0 → F i0 ≤ \max_(i | P i) F i.

-Lemma leq_bigmax (I : finType) F (i0 : I) : F i0 ≤ \max_i F i.
+Lemma leq_bigmax (I : finType) F (i0 : I) : F i0 ≤ \max_i F i.

-Lemma bigmax_leqP (I : finType) (P : pred I) m F :
-  reflect (∀ i, P i → F i ≤ m) (\max_(i | P i) F i ≤ m).
+Lemma bigmax_leqP (I : finType) (P : pred I) m F :
+  reflect (∀ i, P i → F i ≤ m) (\max_(i | P i) F i ≤ m).

-Lemma bigmax_sup (I : finType) i0 (P : pred I) m F :
-  P i0 → m ≤ F i0 → m ≤ \max_(i | P i) F i.
+Lemma bigmax_sup (I : finType) i0 (P : pred I) m F :
+  P i0 → m ≤ F i0 → m ≤ \max_(i | P i) F i.

-Lemma bigmax_eq_arg (I : finType) i0 (P : pred I) F :
-  P i0 → \max_(i | P i) F i = F [arg max_(i > i0 | P i) F i].
+Lemma bigmax_eq_arg (I : finType) i0 (P : pred I) F :
+  P i0 → \max_(i | P i) F i = F [arg max_(i > i0 | P i) F i].

-Lemma eq_bigmax_cond (I : finType) (A : pred I) F :
-  #|A| > 0 → {i0 | i0 \in A & \max_(i in A) F i = F i0}.
+Lemma eq_bigmax_cond (I : finType) (A : pred I) F :
+  #|A| > 0 → {i0 | i0 \in A & \max_(i in A) F i = F i0}.

-Lemma eq_bigmax (I : finType) F : #|I| > 0 → {i0 : I | \max_i F i = F i0}.
+Lemma eq_bigmax (I : finType) F : #|I| > 0 → {i0 : I | \max_i F i = F i0}.

-Lemma expn_sum m I r (P : pred I) F :
-  (m ^ (\sum_(i <- r | P i) F i) = \prod_(i <- r | P i) m ^ F i)%N.
+Lemma expn_sum m I r (P : pred I) F :
+  (m ^ (\sum_(i <- r | P i) F i) = \prod_(i <- r | P i) m ^ F i)%N.

-Lemma dvdn_biglcmP (I : finType) (P : pred I) F m :
-  reflect (∀ i, P i → F i %| m) (\big[lcmn/1%N]_(i | P i) F i %| m).
+Lemma dvdn_biglcmP (I : finType) (P : pred I) F m :
+  reflect (∀ i, P i → F i %| m) (\big[lcmn/1%N]_(i | P i) F i %| m).

-Lemma biglcmn_sup (I : finType) i0 (P : pred I) F m :
-  P i0 → m %| F i0 → m %| \big[lcmn/1%N]_(i | P i) F i.
+Lemma biglcmn_sup (I : finType) i0 (P : pred I) F m :
+  P i0 → m %| F i0 → m %| \big[lcmn/1%N]_(i | P i) F i.

-Lemma dvdn_biggcdP (I : finType) (P : pred I) F m :
-  reflect (∀ i, P i → m %| F i) (m %| \big[gcdn/0]_(i | P i) F i).
+Lemma dvdn_biggcdP (I : finType) (P : pred I) F m :
+  reflect (∀ i, P i → m %| F i) (m %| \big[gcdn/0]_(i | P i) F i).

-Lemma biggcdn_inf (I : finType) i0 (P : pred I) F m :
-  P i0 → F i0 %| m → \big[gcdn/0]_(i | P i) F i %| m.
+Lemma biggcdn_inf (I : finType) i0 (P : pred I) F m :
+  P i0 → F i0 %| m → \big[gcdn/0]_(i | P i) F i %| m.

-Unset Implicit Arguments.
+Notation "@ 'eq_big_perm'" :=
+  (deprecate eq_big_perm perm_big) (at level 10, only parsing).
+ +
+Notation eq_big_perm :=
+  ((fun R idx op I r1 P F r2 ⇒ @eq_big_perm R idx op I r1 r2 P F)
+        _ _ _ _ _ _ _) (only parsing).
-- cgit v1.2.3