Explicit `bigop` enumeration handling

Added lemmas `big_enum_cond`, `big_enum` and `big_enumP` to handle more
explicitly big ops iterating over explicit enumerations in a `finType`.
   The previous practice was to rely on the convertibility between
`enum A` and `filter A (index_enum T)`, sometimes explicitly via the
`filter_index_enum` equality, more often than not implicitly.
  Both are likely to fail after the integration of `finmap`, as the
`choiceType` theory can’t guarantee that the order in selected
enumerations is consistent.
  For this reason `big_enum` and the related (but currently unused)
`big_image` lemmas are restricted to the abelian case. The `big_enumP`
lemma can be used to handle enumerations in the non-abelian case, as
explained in the `bigop.v` internal documentation.
  The Changelog entry enjoins clients to stop relying on either
`filter_index_enum` and convertibility (though this PR still provides
both), and warns about the restriction of the `big_image` lemma set to
the abelian case, as it it a possible source of incompatibility.

16 files changed, 214 insertions, 143 deletions

diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index 38beffc..7e1dfbb 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -2091,7 +2091,7 @@ Lemma mxdirect_delta n f : {in P &, injective f} ->
 Proof.
 pose fP := image f P => Uf; have UfP: uniq fP by apply/dinjectiveP.
 suffices /mxdirectP : mxdirect (\sum_i <<delta_mx 0 i : 'rV[F]_n>>).
-  rewrite /= !(bigID [mem fP] predT) -!big_uniq //= !big_map !big_filter.
+  rewrite /= !(bigID [mem fP] predT) -!big_uniq //= !big_map !big_enum.
   by move/mxdirectP; rewrite mxdirect_addsE => /andP[].
 apply/mxdirectP=> /=; transitivity (mxrank (1%:M : 'M[F]_n)).
   apply/eqmx_rank; rewrite submx1 mx1_sum_delta summx_sub_sums // => i _.
diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v
index 861a7df..c49bec0 100644
--- a/mathcomp/algebra/mxpoly.v
+++ b/mathcomp/algebra/mxpoly.v
@@ -307,16 +307,16 @@ Implicit Types p q : {poly R}.
 Definition char_poly_mx := 'X%:M - map_mx (@polyC R) A.
 Definition char_poly := \det char_poly_mx.
 
-Let diagA := [seq A i i | i : 'I_n].
+Let diagA := [seq A i i | i <- index_enum _ & true].
 Let size_diagA : size diagA = n.
-Proof. by rewrite size_image card_ord. Qed.
+Proof. by rewrite -[n]card_ord size_map; have [e _ _ []] := big_enumP. Qed.
 
 Let split_diagA :
   exists2 q, \prod_(x <- diagA) ('X - x%:P) + q = char_poly & size q <= n.-1.
 Proof.
 rewrite [char_poly](bigD1 1%g) //=; set q := \sum_(s | _) _; exists q.
-  congr (_ + _); rewrite odd_perm1 mul1r big_map enumT; apply: eq_bigr => i _.
-  by rewrite !mxE perm1 eqxx.
+  congr (_ + _); rewrite odd_perm1 mul1r big_map big_filter /=.
+  by apply: eq_bigr => i _; rewrite !mxE perm1 eqxx.
 apply: leq_trans {q}(size_sum _ _ _) _; apply/bigmax_leqP=> s nt_s.
 have{nt_s} [i nfix_i]: exists i, s i != i.
   apply/existsP; rewrite -negb_forall; apply: contra nt_s => s_1.
@@ -329,7 +329,7 @@ apply: leq_trans (_ : #|[pred j | s j == j]|.+1 <= n.-1).
     by rewrite -subn1 -addnS leq_subLR addnA leq_add.
   rewrite !mxE eq_sym !inE; case: (s j == j); first by rewrite polyseqXsubC.
   by rewrite sub0r size_opp size_polyC leq_b1.
-rewrite -{8}[n]card_ord -(cardC (pred2 (s i) i)) card2 nfix_i !ltnS.
+rewrite -[n in n.-1]card_ord -(cardC (pred2 (s i) i)) card2 nfix_i !ltnS.
 apply: subset_leq_card; apply/subsetP=> j; move/(_ =P j)=> fix_j.
 rewrite !inE -{1}fix_j (inj_eq perm_inj) orbb.
 by apply: contraNneq nfix_i => <-; rewrite fix_j.
@@ -354,7 +354,7 @@ Proof.
 move=> n_gt0; have [q <- lt_q_n] := split_diagA; set p := \prod_(x <- _) _.
 rewrite coefD {q lt_q_n}(nth_default 0 lt_q_n) addr0.
 have{n_gt0} ->: p`_n.-1 = ('X * p)`_n by rewrite coefXM eqn0Ngt n_gt0.
-have ->: \tr A = \sum_(x <- diagA) x by rewrite big_map enumT.
+have ->: \tr A = \sum_(x <- diagA) x by rewrite big_map big_filter.
 rewrite -size_diagA {}/p; elim: diagA => [|x d IHd].
   by rewrite !big_nil mulr1 coefX oppr0.
 rewrite !big_cons coefXM mulrBl coefB IHd opprD addrC; congr (- _ + _).
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index 2bb3614..25037e8 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -922,7 +922,10 @@ by rewrite size_XsubC.
 Qed.
 
 Lemma size_exp_XsubC n a : size (('X - a%:P) ^+ n) = n.+1.
-Proof. by rewrite -[n]card_ord -prodr_const size_prod_XsubC cardE enumT. Qed.
+Proof.
+rewrite -[n]card_ord -prodr_const -big_filter size_prod_XsubC.
+by have [e _ _ [_ ->]] := big_enumP.
+Qed.
 
 (* Some facts about regular elements. *)
 
diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v
index 87ca0f4..1f8ad30 100644
--- a/mathcomp/algebra/vector.v
+++ b/mathcomp/algebra/vector.v
@@ -1879,7 +1879,7 @@ Variable (K : fieldType) (vT : vectType K).
 Lemma sumv_pi_sum (I : finType) (P : pred I) Vs v (V : {vspace vT})
                   (defV : V = (\sum_(i | P i) Vs i)%VS) :
   v \in V -> \sum_(i | P i) sumv_pi_for defV i v = v :> vT.
-Proof. by apply: sumv_pi_uniq_sum; apply: enum_uniq. Qed.
+Proof. by apply: sumv_pi_uniq_sum; have [e _ []] := big_enumP. Qed.
 
 Lemma sumv_pi_nat_sum m n (P : pred nat) Vs v (V : {vspace vT})
                       (defV : V = (\sum_(m <= i < n | P i) Vs i)%VS) :
diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v
index c35cdd6..3f461e3 100644
--- a/mathcomp/character/classfun.v
+++ b/mathcomp/character/classfun.v
@@ -528,8 +528,7 @@ Qed.
 Lemma cfun_on_sum A :
   'CF(G, A) = (\sum_(xG in classes G | xG \subset A) <['1_xG]>)%VS.
 Proof.
-rewrite ['CF(G, A)]span_def big_map big_filter.
-by apply: eq_bigl => xG; rewrite !inE.
+by rewrite ['CF(G, A)]span_def big_image; apply: eq_bigl => xG; rewrite !inE.
 Qed.
 
 Lemma cfun_onP A phi :
@@ -2047,15 +2046,14 @@ Lemma cfBigdprodEi i (phi : 'CF(A i)) x :
     P i -> (forall j, P j -> x j \in A j) ->
   cfBigdprodi phi (\prod_(j | P j) x j)%g = phi (x i).
 Proof.
-set r := enum P => Pi /forall_inP; have r_i: i \in r by rewrite mem_enum.
-have:= bigdprodWcp defG; rewrite -big_andE -!(big_filter _ P) filter_index_enum.
-rewrite -/r big_all => defGr /allP Ax.
-rewrite (perm_bigcprod defGr Ax (perm_to_rem r_i)) big_cons cfDprodEl ?Pi //.
-- by rewrite cfRes_id.
-- by rewrite Ax.
-rewrite big_seq group_prod // => j; rewrite mem_rem_uniq ?enum_uniq //.
-case/andP=> i'j /= r_j; apply/mem_gen/bigcupP; exists j; last exact: Ax.
-by rewrite -[P j](mem_enum P) r_j.
+have [r big_r [Ur mem_r] _] := big_enumP P => Pi AxP.
+have:= bigdprodWcp defG; rewrite -!big_r => defGr.
+have{AxP} [r_i Axr]: i \in r /\ {in r, forall j, x j \in A j}.
+  by split=> [|j]; rewrite mem_r // => /AxP.
+rewrite (perm_bigcprod defGr Axr (perm_to_rem r_i)) big_cons.
+rewrite cfDprodEl ?Pi ?cfRes_id ?Axr // big_seq group_prod // => j.
+rewrite mem_rem_uniq // => /andP[i'j /= r_j].
+by apply/mem_gen/bigcupP; exists j; [rewrite -mem_r r_j | apply: Axr].
 Qed.
 
 Lemma cfBigdprodi_iso i : P i -> isometry (@cfBigdprodi i).
diff --git a/mathcomp/character/inertia.v b/mathcomp/character/inertia.v
index d3dfd38..c644150 100644
--- a/mathcomp/character/inertia.v
+++ b/mathcomp/character/inertia.v
@@ -481,7 +481,7 @@ Lemma reindex_cfclass R idx (op : Monoid.com_law idx) (F : 'CF(H) -> R) i :
   \big[op/idx]_(chi <- ('chi_i ^: G)%CF) F chi
      = \big[op/idx]_(j | 'chi_j \in ('chi_i ^: G)%CF) F 'chi_j.
 Proof.
-move/im_cfclass_Iirr/(perm_big _) <-; rewrite big_map big_filter /=.
+move/im_cfclass_Iirr/(perm_big _) <-; rewrite big_image /=.
 by apply: eq_bigl => j; rewrite cfclass_IirrE.
 Qed.
 
@@ -1174,7 +1174,7 @@ have [inj_Mphi | /injectivePn[i [j i'j eq_mm_ij]]] := boolP (injectiveb mmLth).
   rewrite ['Ind phi]cfun_sum_cfdot sum_cfunE (bigID (mem (codom mmLth))) /=.
   rewrite ler_paddr ?sumr_ge0 // => [i _|].
     by rewrite char1_ge0 ?rpredZ_Cnat ?Cnat_cfdot_char ?cfInd_char ?irr_char.
-  rewrite -big_uniq //= big_map big_filter -sumr_const ler_sum // => i _.
+  rewrite -big_uniq //= big_image -sumr_const ler_sum // => i _.
   rewrite cfunE -[in rhs in _ <= rhs](cfRes1 L) -cfdot_Res_r mmLthL cfRes1.
   by rewrite DthL cfdotZr rmorph_nat cfnorm_irr mulr1.
 constructor 2; exists e; first by exists p0.
diff --git a/mathcomp/character/integral_char.v b/mathcomp/character/integral_char.v
index c6d40e2..22bd171 100644
--- a/mathcomp/character/integral_char.v
+++ b/mathcomp/character/integral_char.v
@@ -56,7 +56,7 @@ have Q_Xn1: ('X^n - 1 : {poly Qn}) \is a polyOver 1%AS.
 have splitXn1: splittingFieldFor 1 ('X^n - 1) {:Qn}.
   pose r := codom (fun i : 'I_n => w ^+ i).
   have Dr: 'X^n - 1 = \prod_(y <- r) ('X - y%:P).
-    by rewrite -(factor_Xn_sub_1 prim_w) big_mkord big_map enumT.
+    by rewrite -(factor_Xn_sub_1 prim_w) big_mkord big_image.
   exists r; first by rewrite -Dr eqpxx.
   apply/eqP; rewrite eqEsubv subvf -genQn adjoin_seqSr //; apply/allP=> /=.
   by rewrite andbT -root_prod_XsubC -Dr; apply/unity_rootP/prim_expr_order.
@@ -657,7 +657,7 @@ have Qpi1: pi1 \in Crat.
     have /vlineP[q ->] := mem_galNorm galQn (memvf a).
     by rewrite rmorphZ_num rmorph1 mulr1 Crat_rat.
   rewrite /galNorm rmorph_prod -/calG imItoQ big_imset //=.
-  rewrite /pi1 -(eq_bigl _ _ imItoS) -big_uniq // big_map big_filter /=.
+  rewrite /pi1 -(eq_bigl _ _ imItoS) -big_uniq // big_image /=.
   apply: eq_bigr => k _; have [nuC DnuC] := gQnC (ItoQ k); rewrite DnuC Da.
   have [r ->] := char_sum_irr Nchi; rewrite !sum_cfunE rmorph_sum.
   apply: eq_bigr => i _; have /QnGg[b Db] := irr_char i.
diff --git a/mathcomp/character/vcharacter.v b/mathcomp/character/vcharacter.v
index 4a113b6..72bacc3 100644
--- a/mathcomp/character/vcharacter.v
+++ b/mathcomp/character/vcharacter.v
@@ -464,7 +464,7 @@ Proof.
 move=> Zphi def_n lt_n_4.
 pose S := [seq '[phi, 'chi_i] *: 'chi_i | i in irr_constt phi].
 have def_phi: phi = \sum_(xi <- S) xi.
-  rewrite big_map /= big_filter big_mkcond {1}[phi]cfun_sum_cfdot.
+  rewrite big_image big_mkcond {1}[phi]cfun_sum_cfdot.
   by apply: eq_bigr => i _; rewrite if_neg; case: eqP => // ->; rewrite scale0r.
 have orthS: orthonormal S.
   apply/orthonormalP; split=> [|_ _ /mapP[i phi_i ->] /mapP[j _ ->]].
diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v
index 18fa55a..acafd8f 100644
--- a/mathcomp/field/algebraics_fundamentals.v
+++ b/mathcomp/field/algebraics_fundamentals.v
@@ -216,7 +216,8 @@ have FpxF q: Fpx (q ^ FtoL) = root (q ^ FtoL) x.
 pose p_ (I : {set 'I_n}) := \prod_(i <- enum I) ('X - (r`_i)%:P).
 have{px0 Dp} /ex_minset[I /minsetP[/andP[FpI pIx0] minI]]: exists I, Fpx (p_ I).
   exists setT; suffices ->: p_ setT = p ^ FtoL by rewrite FpxF.
-  by rewrite Dp (big_nth 0) big_mkord /p_ (eq_enum (in_set _)) big_filter.
+  rewrite Dp (big_nth 0) big_mkord /p_ big_enum /=.
+  by apply/eq_bigl=> i; rewrite inE.
 have{p} [p DpI]: {p | p_ I = p ^ FtoL}.
   exists (p_ I ^ (fun y => if isF y is left Fy then sval (sig_eqW Fy) else 0)).
   rewrite -map_poly_comp map_poly_id // => y /(allP FpI) /=.
diff --git a/mathcomp/field/cyclotomic.v b/mathcomp/field/cyclotomic.v
index d80a909..6e7432f 100644
--- a/mathcomp/field/cyclotomic.v
+++ b/mathcomp/field/cyclotomic.v
@@ -39,8 +39,9 @@ Proof. exact: monic_prod_XsubC. Qed.
 
 Lemma size_cyclotomic z n : size (cyclotomic z n) = (totient n).+1.
 Proof.
-rewrite /cyclotomic -big_filter filter_index_enum size_prod_XsubC; congr _.+1.
-rewrite -cardE -sum1_card totient_count_coprime -big_mkcond big_mkord.
+rewrite /cyclotomic -big_filter size_prod_XsubC; congr _.+1.
+case: big_enumP => _ _ _ [_ ->].
+rewrite totient_count_coprime -big_mkcond big_mkord -sum1_card.
 by apply: eq_bigl => k; rewrite coprime_sym.
 Qed.
 
@@ -63,14 +64,13 @@ Let n_gt0 := prim_order_gt0 prim_z.
 
 Lemma root_cyclotomic x : root (cyclotomic z n) x = n.-primitive_root x.
 Proof.
-rewrite /cyclotomic -big_filter filter_index_enum.
-rewrite -(big_map _ xpredT (fun y => 'X - y%:P)) root_prod_XsubC.
+transitivity (x \in [seq z ^+ i | i : 'I_n in [pred i : 'I_n | coprime i n]]).
+  by rewrite -root_prod_XsubC big_image.
 apply/imageP/idP=> [[k co_k_n ->] | prim_x].
   by rewrite prim_root_exp_coprime.
 have [k Dx] := prim_rootP prim_z (prim_expr_order prim_x).
-exists (Ordinal (ltn_pmod k n_gt0)) => /=.
-  by rewrite unfold_in /= coprime_modl -(prim_root_exp_coprime k prim_z) -Dx.
-by rewrite prim_expr_mod.
+exists (Ordinal (ltn_pmod k n_gt0)) => /=; last by rewrite prim_expr_mod.
+by rewrite inE coprime_modl -(prim_root_exp_coprime k prim_z) -Dx.
 Qed.
 
 Lemma prod_cyclotomic :
@@ -212,9 +212,7 @@ Proof.
 have [-> | n_gt0] := posnP n; first by rewrite Cyclotomic0 polyseq1.
 have [z prim_z] := C_prim_root_exists n_gt0.
 rewrite -(size_map_inj_poly (can_inj intCK)) //.
-rewrite (Cintr_Cyclotomic prim_z) -[_ n]big_filter filter_index_enum.
-rewrite size_prod_XsubC -cardE totient_count_coprime big_mkord -big_mkcond /=.
-by rewrite (eq_card (fun _ => coprime_sym _ _)) sum1_card.
+by rewrite (Cintr_Cyclotomic prim_z) size_cyclotomic.
 Qed.
 
 Lemma minCpoly_cyclotomic n z :
@@ -252,8 +250,8 @@ have [zk gzk0]: exists zk, root (pZtoC g) zk.
   by exists rg`_0; rewrite Dg root_prod_XsubC mem_nth.
 have [k cokn Dzk]: exists2 k, coprime k n & zk = z ^+ k.
   have: root pz zk by rewrite -Dpz -Dfg rmorphM rootM gzk0 orbT.
-  rewrite -[pz]big_filter -(big_map _ xpredT (fun a => 'X - a%:P)).
-  by rewrite root_prod_XsubC => /imageP[k]; exists k.
+  rewrite -[pz](big_image _ _ _ (fun r => 'X - r%:P)) root_prod_XsubC.
+  by case/imageP=> k; exists k.
 have co_fg (R : idomainType): n%:R != 0 :> R -> @coprimep R (intrp f) (intrp g).
   move=> nz_n; have: separable_poly (intrp ('X^n - 1) : {poly R}).
     by rewrite rmorphB rmorph1 /= map_polyXn separable_Xn_sub_1.
diff --git a/mathcomp/field/finfield.v b/mathcomp/field/finfield.v
index b184ed7..19871cb 100644
--- a/mathcomp/field/finfield.v
+++ b/mathcomp/field/finfield.v
@@ -99,7 +99,7 @@ set n := #|F|; set oppX := - 'X; set pF := LHS.
 have le_oppX_n: size oppX <= n by rewrite size_opp size_polyX finRing_gt1.
 have: size pF = (size (enum F)).+1 by rewrite -cardE size_addl size_polyXn.
 move/all_roots_prod_XsubC->; last by rewrite uniq_rootsE enum_uniq.
-  by rewrite enumT lead_coefDl ?size_polyXn // lead_coefXn scale1r.
+  by rewrite big_enum lead_coefDl ?size_polyXn // lead_coefXn scale1r.
 by apply/allP=> x _; rewrite rootE !hornerE hornerXn expf_card subrr.
 Qed.
 
@@ -186,7 +186,7 @@ Canonical fieldExt_finFieldType fT := [finFieldType of fT].
 Lemma finField_splittingField_axiom fT : SplittingField.axiom fT.
 Proof.
 exists ('X^#|fT| - 'X); first by rewrite rpredB 1?rpredX ?polyOverX.
-exists (enum fT); first by rewrite enumT finField_genPoly eqpxx.
+exists (enum fT); first by rewrite big_enum finField_genPoly eqpxx.
 by apply/vspaceP=> x; rewrite memvf seqv_sub_adjoin ?mem_enum.
 Qed.
 
@@ -363,9 +363,10 @@ without loss {K} ->: K / K = 1%AS.
   by move=> IH_K; apply: galoisS (IH_K _ (erefl _)); rewrite sub1v subvf.
 apply/splitting_galoisField; pose finL := FinFieldExtType L.
 exists ('X^#|finL| - 'X); split; first by rewrite rpredB 1?rpredX ?polyOverX.
-  rewrite (finField_genPoly finL) -big_filter.
+  rewrite (finField_genPoly finL) -big_enum /=.
   by rewrite separable_prod_XsubC ?(enum_uniq finL).
-exists (enum finL); first by rewrite enumT (finField_genPoly finL) eqpxx.
+exists (enum finL).
+  by rewrite (@big_enum _ _ _ _ finL) (finField_genPoly finL) eqpxx.
 by apply/vspaceP=> x; rewrite memvf seqv_sub_adjoin ?(mem_enum finL).
 Qed.
 
@@ -390,7 +391,7 @@ have idfP x: reflect (f x = x) (x \in 1%VS).
     rewrite /q rmorphB /= map_polyXn map_polyX.
     by rewrite rootE !(hornerE, hornerXn) [x ^+ _]xFx subrr.
   have{q} ->: q = \prod_(z <- [seq b%:A | b : F]) ('X - z%:P).
-    rewrite /q finField_genPoly rmorph_prod big_map enumT.
+    rewrite /q finField_genPoly rmorph_prod big_image /=.
     by apply: eq_bigr => b _; rewrite rmorphB /= map_polyX map_polyC.
   by rewrite root_prod_XsubC => /mapP[a]; exists a.
 have fM: rmorphism f.
diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v
index 4aaef57..72cd0df 100644
--- a/mathcomp/field/galois.v
+++ b/mathcomp/field/galois.v
@@ -448,14 +448,15 @@ pose mkf (z : L) := 'X - z%:P.
 exists (\prod_i \prod_(j < \dim {:L} | j < size (r i)) mkf (r i)`_j).
   apply: rpred_prod => i _; rewrite big_ord_narrow /= /r; case: sigW => rs /=.
   by rewrite (big_nth 0) big_mkord => /eqP <- {rs}; apply: minPolyOver.
-rewrite pair_big_dep /= -big_filter filter_index_enum -(big_map _ xpredT mkf).
+rewrite pair_big_dep /= -big_filter -(big_map _ xpredT mkf).
 set rF := map _ _; exists rF; first exact: eqpxx.
 apply/eqP; rewrite eqEsubv subvf -(span_basis (vbasisP {:L})).
 apply/span_subvP=> _ /tnthP[i ->]; set x := tnth _ i.
 have /tnthP[j ->]: x \in in_tuple (r i).
   by rewrite -root_prod_XsubC /r; case: sigW => _ /=/eqP<-; apply: root_minPoly.
-apply/seqv_sub_adjoin/imageP; rewrite (tnth_nth 0) /in_mem/=.
-by exists (i, widen_ord (sz_r i) j) => /=.
+apply/seqv_sub_adjoin/mapP; rewrite (tnth_nth 0).
+exists (i, widen_ord (sz_r i) j) => //.
+by rewrite mem_filter /= ltn_ord mem_index_enum.
 Qed.
 
 Fact regular_splittingAxiom F : SplittingField.axiom (regular_fieldExtType F).
diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v
index ac785a3..699a1ba 100644
--- a/mathcomp/fingroup/fingroup.v
+++ b/mathcomp/fingroup/fingroup.v
@@ -1,7 +1,7 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice.
-From mathcomp Require Import fintype div path bigop prime finset.
+From mathcomp Require Import fintype div path tuple bigop prime finset.
 
 (******************************************************************************)
 (* This file defines the main interface for finite groups :                   *)
@@ -858,14 +858,13 @@ Lemma prodsgP (I : finType) (P : pred I) (A : I -> {set gT}) x :
   reflect (exists2 c, forall i, P i -> c i \in A i & x = \prod_(i | P i) c i)
           (x \in \prod_(i | P i) A i).
 Proof.
-rewrite -big_filter filter_index_enum; set r := enum P.
-pose inA c := all (fun i => c i \in A i); set piAx := x \in _.
-suffices IHr: reflect (exists2 c, inA c r & x = \prod_(i <- r) c i) piAx.
-  apply: (iffP IHr) => -[c inAc ->]; do [exists c; last by rewrite big_filter].
-    by move=> i Pi; rewrite (allP inAc) ?mem_enum.
-  by apply/allP=> i; rewrite mem_enum => /inAc.
-have: uniq r by rewrite enum_uniq.
-elim: {P}r x @piAx => /= [x _ | i r IHr x /andP[r'i /IHr{IHr}IHr]].
+have [r big_r [Ur mem_r] _] := big_enumP P.
+pose inA c := all (fun i => c i \in A i); rewrite -big_r; set piAx := x \in _.
+suffices{big_r} IHr: reflect (exists2 c, inA c r & x = \prod_(i <- r) c i) piAx.
+  apply: (iffP IHr) => -[c inAc ->]; do [exists c; last by rewrite big_r].
+    by move=> i Pi; rewrite (allP inAc) ?mem_r.
+  by apply/allP=> i; rewrite mem_r => /inAc.
+elim: {P mem_r}r x @piAx Ur => /= [x _ | i r IHr x /andP[r'i /IHr{IHr}IHr]].
   by rewrite unlock; apply: (iffP set1P) => [-> | [] //]; exists (fun=> x).
 rewrite big_cons; apply: (iffP idP) => [|[c /andP[Aci Ac] ->]]; last first.
   by rewrite big_cons mem_mulg //; apply/IHr=> //; exists c.
@@ -2174,19 +2173,14 @@ Lemma gen_prodgP A x :
 Proof.
 apply: (iffP idP) => [|[n [c Ac ->]]]; last first.
   by apply: group_prod => i _; rewrite mem_gen ?Ac.
-have [n ->] := gen_expgs A; rewrite /expgn /expgn_rec Monoid.iteropE.
-have ->: n = count 'I_n (index_enum _).
-  by rewrite -size_filter filter_index_enum -cardT card_ord.
-rewrite -big_const_seq; case/prodsgP=> /= c Ac def_x.
+have [n ->] := gen_expgs A; rewrite /expgn /expgn_rec Monoid.iteropE /=.
+rewrite -[n]card_ord -big_const => /prodsgP[/= c Ac def_x]. 
 have{Ac def_x} ->: x = \prod_(i | c i \in A) c i.
   rewrite big_mkcond {x}def_x; apply: eq_bigr => i _.
   by case/setU1P: (Ac i isT) => -> //; rewrite if_same.
-rewrite -big_filter; set e := filter _ _; case def_e: e => [|i e'].
-  by exists 0; exists (fun _ => 1) => [[] // |]; rewrite big_nil big_ord0.
-rewrite -{e'}def_e (big_nth i) big_mkord.
-exists (size e); exists (c \o nth i e \o val) => // j /=.
-have: nth i e j \in e by rewrite mem_nth.
-by rewrite mem_filter; case/andP.
+have [e <- [_ /= mem_e] _] := big_enumP [preim c of A].
+pose t := in_tuple e; rewrite -[e]/(val t) big_tuple.
+by exists (size e), (c \o tnth t) => // i; rewrite -mem_e mem_tnth.
 Qed.
 
 Lemma genD A B : A \subset <<A :\: B>> -> <<A :\: B>> = <<A>>.
diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v
index 8357bc4..b1181c0 100644
--- a/mathcomp/fingroup/gproduct.v
+++ b/mathcomp/fingroup/gproduct.v
@@ -634,13 +634,13 @@ Lemma reindex_bigcprod (I J : finType) (h : J -> I) P (A : I -> {set gT}) G x :
     {in SimplPred P, forall i, x i \in A i} ->
   \prod_(i | P i) x i = \prod_(j | P (h j)) x (h j).
 Proof.
-case=> h1 hK h1K; rewrite -!(big_filter _ P) filter_index_enum => defG Ax.
-rewrite -(big_map h P x) -(big_filter _ P) filter_map filter_index_enum.
-apply: perm_bigcprod defG _ _ => [i|]; first by rewrite mem_enum => /Ax.
-apply: uniq_perm (enum_uniq P) _ _ => [|i].
-  by apply/dinjectiveP; apply: (can_in_inj hK).
-rewrite mem_enum; apply/idP/imageP=> [Pi | [j Phj ->//]].
-by exists (h1 i); rewrite ?inE h1K.
+case=> h1 hK h1K defG Ax; have [e big_e [Ue mem_e] _] := big_enumP P.
+rewrite -!big_e in defG *; rewrite -(big_map h P x) -[RHS]big_filter filter_map.
+apply: perm_bigcprod defG _ _ => [i|]; first by rewrite mem_e => /Ax.
+have [r _ [Ur /= mem_r] _] := big_enumP; apply: uniq_perm Ue _ _ => [|i].
+  by rewrite map_inj_in_uniq // => i j; rewrite !mem_r ; apply: (can_in_inj hK).
+rewrite mem_e; apply/idP/mapP=> [Pi|[j r_j ->]]; last by rewrite -mem_r.
+by exists (h1 i); rewrite ?mem_r h1K.
 Qed.
 
 (* Direct product *)
@@ -849,18 +849,20 @@ Lemma mem_bigdprod (I : finType) (P : pred I) F G x :
                 forall i, P i -> e i = c i].
 Proof.
 move=> defG; rewrite -(bigdprodW defG) => /prodsgP[c Fc ->].
-exists c; split=> // e Fe eq_ce i Pi.
-set r := index_enum _ in defG eq_ce.
-have: i \in r by rewrite -[r]enumT mem_enum.
-elim: r G defG eq_ce => // j r IHr G; rewrite !big_cons inE.
-case Pj: (P j); last by case: eqP (IHr G) => // eq_ij; rewrite eq_ij Pj in Pi.
-case/dprodP=> [[K H defK defH] _ _]; rewrite defK defH => tiFjH eq_ce.
-suffices{i Pi IHr} eq_cej: c j = e j.
-  case/predU1P=> [-> //|]; apply: IHr defH _.
+have [r big_r [_ mem_r] _] := big_enumP P.
+exists c; split=> // e Fe eq_ce i Pi; rewrite -!{}big_r in defG eq_ce.
+have{Pi}: i \in r by rewrite mem_r.
+have{mem_r}: all P r by apply/allP=> j; rewrite mem_r.
+elim: r G defG eq_ce => // j r IHr G.
+rewrite !big_cons inE /= => /dprodP[[K H defK defH] _ _].
+rewrite defK defH => tiFjH eq_ce /andP[Pj Pr].
+suffices{i IHr} eq_cej: c j = e j.
+  case/predU1P=> [-> //|]; apply: IHr defH _ Pr.
   by apply: (mulgI (c j)); rewrite eq_ce eq_cej.
 rewrite !(big_nth j) !big_mkord in defH eq_ce.
-move/(congr1 (divgr K H)) : eq_ce; move/bigdprodW: defH => defH.
-by rewrite !divgrMid // -?defK -?defH ?mem_prodg // => *; rewrite ?Fc ?Fe.
+move/(congr1 (divgr K H)): eq_ce; move/bigdprodW: defH => defH.
+move/(all_nthP j) in Pr.
+by rewrite !divgrMid // -?defK -?defH ?mem_prodg // => *; rewrite ?Fc ?Fe ?Pr.
 Qed.
 
 End InternalProd.
diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v
index f596c3f..8bdbe60 100644
--- a/mathcomp/ssreflect/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
@@ -545,20 +545,35 @@ Canonical bigop_unlock := Unlockable BigOp.bigopE.
 
 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).
 Proof.
 rewrite mem_iota; case le_m_i: (m <= i) => //=.
 by rewrite -leq_subLR subSn // -subn_gt0 -subnDA subnKC // subn_gt0.
 Qed.
 
+(* Legacy mathcomp scripts have been relying on the fact that enum A and      *)
+(* filter A (index_enum T) are convertible. This is likely to change in the   *)
+(* next mathcomp release when enum, pick, subset and card are generalised to  *)
+(* predicates with finite support in a choiceType - in fact the two will only *)
+(* be equal up to permutation in this new theory.                             *)
+(*  It is therefore advisable to stop relying on this, and use the new        *)
+(* facilities provided in this library: lemmas big_enumP, big_enum, big_image *)
+(* and such. Users wishing to test compliance should change the Defined in    *)
+(* index_enum_key to Qed, and comment out the filter_index_enum compatibility *)
+(* definition below (or Import Deprecation.Reject).                           *)
+Fact index_enum_key : unit. Proof. split. Defined. (* Qed. *)
+Definition index_enum (T : finType) :=
+  locked_with index_enum_key (Finite.enum T).
+
+Lemma deprecated_filter_index_enum T P : filter P (index_enum T) = enum P.
+Proof. by rewrite [index_enum T]unlock. Qed.
+
 Lemma mem_index_enum T i : i \in index_enum T.
-Proof. by rewrite -[index_enum T]enumT mem_enum. Qed.
+Proof. by rewrite [index_enum T]unlock -enumT mem_enum. Qed.
 Hint Resolve mem_index_enum : core.
 
-Lemma filter_index_enum T P : filter P (index_enum T) = enum P.
-Proof. by []. Qed.
+Lemma index_enum_uniq T : uniq (index_enum T).
+Proof. by rewrite [index_enum T]unlock -enumT enum_uniq. Qed.
 
 Notation "\big [ op / idx ]_ ( i <- r | P ) F" :=
   (bigop idx r (fun i => BigBody i op P%B F)) : big_scope.
@@ -872,10 +887,6 @@ rewrite -big_filter -(big_filter r2) filter_cat.
 by rewrite has_count -size_filter; case: filter.
 Qed.
 
-Lemma big_const_seq r (P : pred I) x :
-  \big[op/idx]_(i <- r | P i) x = iter (count P r) (op x) idx.
-Proof. by rewrite unlock; elim: r => //= i r ->; case: (P i). Qed.
-
 End SeqExtension.
 
 Lemma big_map_id J (h : J -> R) r (P : pred R) :
@@ -971,7 +982,7 @@ 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.
 Proof.
 rewrite /index_iota subn0 -(big_map (@nat_of_ord n)).
-by congr bigop; rewrite /index_enum unlock val_ord_enum.
+by congr bigop; rewrite /index_enum 2!unlock val_ord_enum.
 Qed.
 
 Lemma big_nat_widen m n1 n2 (P : pred nat) F :
@@ -1070,45 +1081,72 @@ rewrite big_ltn // big_add1 /= big_mkord; congr op.
 by apply: eq_bigr => i _; rewrite eqFG.
 Qed.
 
-Lemma big_const (I : finType) (A : pred I) x :
-  \big[op/idx]_(i in A) x = iter #|A| (op x) idx.
-Proof. by rewrite big_const_seq -size_filter cardE. Qed.
-
-Lemma big_const_nat m n x :
-  \big[op/idx]_(m <= i < n) x = iter (n - m) (op x) idx.
-Proof. by rewrite big_const_seq count_predT size_iota. Qed.
-
-Lemma big_const_ord n x :
-  \big[op/idx]_(i < n) x = iter n (op x) idx.
-Proof. by rewrite big_const card_ord. Qed.
-
 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.
+  \big[op/idx]_(i <- nseq n a | P i) F i
+    = if P a then iter n (op (F a)) idx else idx.
 Proof. by rewrite unlock; elim: n => /= [|n ->]; case: (P a). Qed.
 
 Lemma big_nseq I n a (F : I -> R):
   \big[op/idx]_(i <- nseq n a) F i = iter n (op (F a)) idx.
 Proof. exact: big_nseq_cond. Qed.
 
-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).
-Proof. by rewrite big_map big_filter_cond. Qed.
+End Extensionality.
 
-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).
-Proof. by rewrite big_map big_filter. Qed.
+Variant big_enum_spec (I : finType) (P : pred I) : seq I -> Type :=
+  BigEnumSpec e of
+    forall R idx op (F : I -> R),
+      \big[op/idx]_(i <- e) F i = \big[op/idx]_(i | P i) F i
+  & uniq e /\ (forall i, i \in e = P i)
+  & (let cP := [pred i | P i] in perm_eq e (enum cP) /\ size e = #|cP|)
+  : big_enum_spec P e.
+
+(*   This lemma can be used to introduce an enumeration into a non-abelian    *)
+(* bigop, in one of three ways:                                               *)
+(*   have [e big_e [Ue mem_e] [e_enum size_e]] := big_enumP P.                *)
+(* gives a permutation e of enum P alongside a equation big_e for converting  *)
+(* between bigops iterating on (i <- e) and ones on (i | P i). Usually not    *)
+(* all properties of e are needed, but see below the big_distr_big_dep proof  *)
+(* where most are.                                                            *)
+(*   rewrite -big_filter; have [e ...] := big_enumP.                          *)
+(* uses big_filter to do this conversion first, and then abstracts the        *)
+(* resulting filter P (index_enum T) enumeration as an e with the same        *)
+(* properties (see big_enum_cond below for an example of this usage).         *)
+(*   Finally                                                                  *)
+(*   rewrite -big_filter; case def_e: _ / big_enumP => [e ...]                *)
+(* does the same while remembering the definition of e.                       *)
+
+Lemma big_enumP I P : big_enum_spec P (filter P (index_enum I)).
+Proof.
+set e := filter P _; have Ue: uniq e by apply/filter_uniq/index_enum_uniq.
+have mem_e i: i \in e = P i by rewrite mem_filter mem_index_enum andbT.
+split=> // [R idx op F | cP]; first by rewrite big_filter.
+suffices De: perm_eq e (enum cP) by rewrite (perm_size De) cardE.
+by apply/uniq_perm=> // [|i]; rewrite ?enum_uniq ?mem_enum ?mem_e.
+Qed.
 
-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.
-Proof. exact: big_image_cond. Qed.
+Section BigConst.
 
-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.
-Proof. exact: big_image. Qed.
+Variables (R : Type) (idx : R) (op : R -> R -> R).
 
-End Extensionality.
+Lemma big_const_seq I r (P : pred I) x :
+  \big[op/idx]_(i <- r | P i) x = iter (count P r) (op x) idx.
+Proof. by rewrite unlock; elim: r => //= i r ->; case: (P i). Qed.
+
+Lemma big_const (I : finType) (A : {pred I}) x :
+  \big[op/idx]_(i in A) x = iter #|A| (op x) idx.
+Proof.
+by have [e <- _ [_ <-]] := big_enumP A; rewrite big_const_seq count_predT.
+Qed.
+
+Lemma big_const_nat m n x :
+  \big[op/idx]_(m <= i < n) x = iter (n - m) (op x) idx.
+Proof. by rewrite big_const_seq count_predT size_iota. Qed.
+
+Lemma big_const_ord n x :
+  \big[op/idx]_(i < n) x = iter n (op x) idx.
+Proof. by rewrite big_const card_ord. Qed.
+
+End BigConst.
 
 Section MonoidProperties.
 
@@ -1214,7 +1252,10 @@ Proof. exact: big_allpairs_dep. Qed.
 
 Lemma big_pred1_eq (I : finType) (i : I) F :
   \big[*%M/1]_(j | j == i) F j = F i.
-Proof. by rewrite -big_filter filter_index_enum enum1 big_seq1. Qed.
+Proof.
+have [e1 <- _ [e_enum _]] := big_enumP (pred1 i).
+by rewrite (perm_small_eq _ e_enum) enum1 ?big_seq1.
+Qed.
 
 Lemma big_pred1 (I : finType) i (P : pred I) F :
   P =1 pred1 i -> \big[*%M/1]_(j | P j) F j = F i.
@@ -1251,7 +1292,7 @@ Lemma big_sumType (I1 I2 : finType) (P : pred (I1 + I2)) F :
         (\big[*%M/1]_(i | P (inl _ i)) F (inl _ i))
       * (\big[*%M/1]_(i | P (inr _ i)) F (inr _ i)).
 Proof.
-by rewrite /index_enum {1}[@Finite.enum]unlock /= big_cat !big_map.
+by rewrite ![index_enum _]unlock [@Finite.enum in LHS]unlock big_cat !big_map.
 Qed.
 
 Lemma big_split_ord m n (P : pred 'I_(m + n)) F :
@@ -1261,8 +1302,8 @@ Lemma big_split_ord m n (P : pred 'I_(m + n)) F :
 Proof.
 rewrite -(big_map _ _ (lshift n) _ P F) -(big_map _ _ (@rshift m _) _ P F).
 rewrite -big_cat; congr bigop; apply: (inj_map val_inj).
-rewrite /index_enum -!enumT val_enum_ord map_cat -map_comp val_enum_ord.
-rewrite -map_comp (map_comp (addn m)) val_enum_ord.
+rewrite map_cat -!map_comp (map_comp (addn m)) /=.
+rewrite ![index_enum _]unlock unlock !val_ord_enum.
 by rewrite -iota_addl addn0 iota_add.
 Qed.
 
@@ -1295,11 +1336,21 @@ rewrite mulmCA; congr (_ * _); rewrite -big_cat; apply: IHr1 => a.
 by move/(_ a): eq_r12; rewrite !count_cat /= addnCA; apply: addnI.
 Qed.
 
+Lemma big_enum_cond (I : finType) (A : {pred I}) (P : pred I) F :
+  \big[*%M/1]_(i <- enum A | P i) F i = \big[*%M/1]_(i in A | P i) F i.
+Proof.
+by rewrite -big_filter_cond; have [e _ _ [/perm_big->]] := big_enumP.
+Qed.
+
+Lemma big_enum (I : finType) (A : {pred I}) F :
+  \big[*%M/1]_(i <- enum A) F i = \big[*%M/1]_(i in A) F i.
+Proof. by rewrite big_enum_cond big_andbC. Qed.
+
 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.
 Proof.
-move=> uniq_r; rewrite -(big_filter _ _ _ (mem r)); apply: perm_big.
-by rewrite filter_index_enum uniq_perm ?enum_uniq // => i; rewrite mem_enum.
+move=> uniq_r; rewrite -big_enum; apply: perm_big.
+by rewrite uniq_perm ?enum_uniq // => i; rewrite mem_enum.
 Qed.
 
 Lemma big_rem (I : eqType) r x (P : pred I) F :
@@ -1403,6 +1454,24 @@ Qed.
 
 Arguments partition_big [I J P] p Q [F].
 
+Lemma big_image_cond I (J : finType) (h : J -> I) (A : pred J) (P : pred I) F :
+  \big[*%M/1]_(i <- [seq h j | j in A] | P i) F i
+     = \big[*%M/1]_(j in A | P (h j)) F (h j).
+Proof. by rewrite big_map big_enum_cond. Qed.
+
+Lemma big_image I (J : finType) (h : J -> I) (A : pred J) F :
+  \big[*%M/1]_(i <- [seq h j | j in A]) F i = \big[*%M/1]_(j in A) F (h j).
+Proof. by rewrite big_map big_enum. Qed.
+
+Lemma big_image_cond_id (J : finType) (h : J -> R) (A : pred J) (P : pred R) :
+  \big[*%M/1]_(i <- [seq h j | j in A] | P i) i
+    = \big[*%M/1]_(j in A | P (h j)) h j.
+Proof. exact: big_image_cond. Qed.
+
+Lemma big_image_id (J : finType) (h : J -> R) (A : pred J) :
+  \big[*%M/1]_(i <- [seq h j | j in A]) i = \big[*%M/1]_(j in A) h j.
+Proof. exact: big_image. Qed.
+
 Lemma reindex_onto (I J : finType) (h : J -> I) h' (P : pred I) F :
    (forall i, P i -> h (h' i) = i) ->
   \big[*%M/1]_(i | P i) F i =
@@ -1635,13 +1704,11 @@ Lemma big_distr_big_dep (I J : finType) j0 (P : pred I) (Q : I -> pred J) F :
      \big[+%M/0]_(f in pfamily j0 P Q) \big[*%M/1]_(i | P i) F i (f i).
 Proof.
 pose fIJ := {ffun I -> J}; pose Pf := pfamily j0 (_ : seq I) Q.
-rewrite -big_filter filter_index_enum; set r := enum P; symmetry.
-transitivity (\big[+%M/0]_(f in Pf r) \big[*%M/1]_(i <- r) F i (f i)).
-  apply: eq_big => f; last by rewrite -big_filter filter_index_enum.
-  by apply: eq_forallb => i; rewrite /= mem_enum.
-have: uniq r by apply: enum_uniq.
-elim: {P}r => /= [_ | i r IHr].
-  rewrite (big_pred1 [ffun => j0]) ?big_nil //= => f.
+have [r big_r [Ur mem_r] _] := big_enumP P.
+symmetry; transitivity (\big[+%M/0]_(f in Pf r) \big[*%M/1]_(i <- r) F i (f i)).
+  by apply: eq_big => // f; apply: eq_forallb => i; rewrite /= mem_r.
+rewrite -{P mem_r}big_r; elim: r Ur => /= [_ | i r IHr].
+  rewrite (big_pred1 [ffun=> j0]) ?big_nil //= => f.
   apply/familyP/eqP=> /= [Df |->{f} i]; last by rewrite ffunE !inE.
   by apply/ffunP=> i; rewrite ffunE; apply/eqP/Df.
 case/andP=> /negbTE nri; rewrite big_cons big_distrl => {IHr}/IHr <-.
@@ -1674,14 +1741,16 @@ 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).
 Proof.
-case: (pickP J) => [j0 _ | J0]; first exact: (big_distr_big_dep j0).
-rewrite {1 4}/index_enum -enumT; case: (enum I) (mem_enum I) => [I0 | i r _].
-  have f0: I -> J by move=> i; have:= I0 i.
-  rewrite (big_pred1 (finfun f0)) ?big_nil // => g.
-  by apply/familyP/eqP=> _; first apply/ffunP; move => i; have:= I0 i.
-have Q0 i': Q i' =1 pred0 by move=> j; have:= J0 j.
-rewrite big_cons /= big_pred0 // mul0m big_pred0 // => f.
-by apply/familyP=> /(_ i); rewrite [_ \in _]Q0.
+have [j _ | J0] := pickP J; first by rewrite (big_distr_big_dep j).
+have Q0 i: Q i =i pred0 by move=> /J0/esym/notF[].
+transitivity (iter #|I| ( *%M 0) 1).
+  by rewrite -big_const; apply/eq_bigr=> i; have /(big_pred0 _)-> := Q0 i.  
+have [i _ | I0] := pickP I.
+  rewrite (cardD1 i) //= mul0m big_pred0 // => f.
+  by apply/familyP=> /(_ i); rewrite Q0.
+have f: I -> J by move=> /I0/esym/notF[].
+rewrite eq_card0 // (big_pred1 (finfun f)) ?big_pred0 // => g.
+by apply/familyP/eqP=> _; first apply/ffunP; move=> /I0/esym/notF[].
 Qed.
 
 Lemma bigA_distr_big (I J : finType) (Q : pred J) (F : I -> J -> R) :
@@ -1874,3 +1943,7 @@ Notation "@ 'eq_big_perm'" :=
 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).
+
+Notation filter_index_enum :=
+  ((fun _ => @deprecated_filter_index_enum _)
+     (deprecate filter_index_enum big_enumP)) (only parsing).
diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v
index 8bdb426..1649a89 100644
--- a/mathcomp/ssreflect/binomial.v
+++ b/mathcomp/ssreflect/binomial.v
@@ -386,8 +386,8 @@ rewrite -card_uniq_tuples.
 have bijFF: {on (_ : pred _), bijective (@Finfun D T)}.
   by exists fgraph => x _; [apply: FinfunK | apply: fgraphK].
 rewrite -(on_card_preimset (bijFF _)); apply: eq_card => /= t.
-rewrite !inE -(big_andE predT) -big_filter big_all -all_map.
-by rewrite -[injectiveb _]/(uniq _) [map _ _]codom_ffun FinfunK.
+rewrite !inE -(big_andE predT) -big_image /= big_all.
+by rewrite -[t in RHS]FinfunK -codom_ffun.
 Qed.
 
 Lemma card_inj_ffuns D T :