3 files changed, 42 insertions, 18 deletions
diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v
index 1b580c0..ee3aedb 100644
--- a/mathcomp/ssreflect/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
@@ -1464,18 +1464,29 @@ 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) ->
+Lemma reindex_omap (I J : finType) (h : J -> I) h' (P : pred I) F :
+    (forall i, P i -> omap h (h' i) = some i) ->
   \big[*%M/1]_(i | P i) F i =
-    \big[*%M/1]_(j | P (h j) && (h' (h j) == j)) F (h j).
+    \big[*%M/1]_(j | P (h j) && (h' (h j) == some j)) F (h j).
 Proof.
 move=> h'K; have [n lePn] := ubnP #|P|; elim: n => // n IHn in P h'K lePn *.
 case: (pickP P) => [i Pi | P0]; last first.
   by rewrite !big_pred0 // => j; rewrite P0.
-rewrite (bigD1 i Pi) (bigD1 (h' i)) h'K ?Pi ?eqxx //=; congr (_ * _).
-rewrite {}IHn => [|j /andP[]|]; [|by auto | by rewrite (cardD1x i) in lePn]. 
-apply: eq_bigl => j; rewrite andbC -andbA (andbCA (P _)); case: eqP => //= hK.
-by congr (_ && ~~ _); apply/eqP/eqP=> [<-|->] //; rewrite h'K.
+have := h'K i Pi; case h'i_eq : (h' i) => [/= j|//] [hj_eq].
+rewrite (bigD1 i Pi) (bigD1 j) hj_eq ?Pi ?h'i_eq ?eqxx //=; congr (_ * _).
+rewrite {}IHn => [|k /andP[]|]; [|by auto | by rewrite (cardD1x i) in lePn].
+apply: eq_bigl => k; rewrite andbC -andbA (andbCA (P _)); case: eqP => //= hK.
+congr (_ && ~~ _); apply/eqP/eqP => [|->//].
+by move=> /(congr1 h'); rewrite h'i_eq hK => -[].
+Qed.
+Arguments reindex_omap [I J] h h' [P F].
+
+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 =
+    \big[*%M/1]_(j | P (h j) && (h' (h j) == j)) F (h j).
+Proof.
+by move=> h'K; rewrite (reindex_omap h (some \o h'))//= => i Pi; rewrite h'K.
 Qed.
 Arguments reindex_onto [I J] h h' [P F].
 
@@ -1493,6 +1504,15 @@ Lemma reindex_inj (I : finType) (h : I -> I) (P : pred I) F :
 Proof. by move=> injh; apply: reindex (onW_bij _ (injF_bij injh)). Qed.
 Arguments reindex_inj [I h P F].
 
+Lemma bigD1_ord n j (P : pred 'I_n) F :
+  P j -> \big[*%M/1]_(i < n | P i) F i
+    = F j * \big[*%M/1]_(i < n.-1 | P (lift j i)) F (lift j i).
+Proof.
+move=> Pj; rewrite (bigD1 j Pj) (reindex_omap (lift j) (unlift j))/=.
+  by under eq_bigl do rewrite liftK eq_sym eqxx neq_lift ?andbT.
+by move=> i; case: unliftP => [k ->|->]; rewrite ?eqxx ?andbF.
+Qed.
+
 Lemma big_enum_val_cond (I : finType) (A : pred I) (P : pred I) F :
   \big[op/idx]_(x in A | P x) F x =
   \big[op/idx]_(i < #|A| | P (enum_val i)) F (enum_val i).
@@ -1656,7 +1676,9 @@ Arguments bigID [R idx op I r].
 Arguments bigU [R idx op I].
 Arguments bigD1 [R idx op I] j [P F].
 Arguments bigD1_seq [R idx op I r] j [F].
+Arguments bigD1_ord [R idx op n] j [P F].
 Arguments partition_big [R idx op I J P] p Q [F].
+Arguments reindex_omap [R idx op I J] h h' [P F].
 Arguments reindex_onto [R idx op I J] h h' [P F].
 Arguments reindex [R idx op I J] h [P F].
 Arguments reindex_inj [R idx op I h P F].
@@ -1749,7 +1771,7 @@ Proof.
 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.  
+  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.
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index 9bd8c1f..4262ed7 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -1453,17 +1453,13 @@ Lemma big_imset h (A : {pred I}) G : {in A &, injective h} ->
   \big[aop/idx]_(j in h @: A) G j = \big[aop/idx]_(i in A) G (h i).
 Proof.
 move=> injh; pose hA := mem (image h A).
-have [x0 Ax0 | A0] := pickP A; last first.
-  by rewrite !big_pred0 // => x; apply/imsetP=> [[i]]; rewrite unfold_in A0.
 rewrite (eq_bigl hA) => [|j]; last exact/imsetP/imageP.
-pose h' j := if insub j : {? j | hA j} is Some u then iinv (svalP u) else x0.
-rewrite (reindex_onto h h') => [|j hAj]; rewrite {}/h'; last first.
-  by rewrite (insubT hA hAj) f_iinv.
-apply: eq_bigl => i; case: insubP => [u -> /= def_u | nhAhi].
-  set i' := iinv _; have Ai' : i' \in A := mem_iinv (svalP u).
-  by apply/eqP/idP=> [<- // | Ai]; apply: injh; rewrite ?f_iinv.
-symmetry; rewrite (negbTE nhAhi); apply/idP=> Ai.
-by case/imageP: nhAhi; exists i.
+pose h' := omap (fun u : {j | hA j} => iinv (svalP u)) \o insub.
+rewrite (reindex_omap h h') => [|j hAj]; rewrite {}/h'/= ?insubT/= ?f_iinv//.
+apply: eq_bigl => i; case: insubP => [u -> /= def_u | nhAhi]; last first.
+  by apply/andP/idP => [[]//| Ai]; case/imageP: nhAhi; exists i.
+set i' := iinv _; have Ai' : i' \in A := mem_iinv (svalP u).
+by apply/eqP/idP => [[<-] // | Ai]; congr Some; apply: injh; rewrite ?f_iinv.
 Qed.
 
 Lemma big_imset_cond h (A : {pred I}) (P : pred J) G : {in A &, injective h} ->
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 88d0f92..3472a1d 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -2074,6 +2074,12 @@ Qed.
 Lemma neq_lift n (h : 'I_n) i : h != lift h i.
 Proof. exact: neq_bump. Qed.
 
+Lemma eq_liftF n (h : 'I_n) i : (h == lift h i) = false.
+Proof. exact/negbTE/neq_lift. Qed.
+
+Lemma lift_eqF n (h : 'I_n) i : (lift h i == h) = false.
+Proof. by rewrite eq_sym eq_liftF. Qed.
+
 Lemma unlift_none n (h : 'I_n) : unlift h h = None.
 Proof. by case: unliftP => // j Dh; case/eqP: (neq_lift h j). Qed.