proposition: Lemma partition_big (I J : finType) (P : pred I) p (Q : pred J) (F : I -> X) : (forall 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.
proof: Proof. move=> Qp; transitivity (\big[*%M/1]_(i | P i && Q (p i)) F i). by apply: eqv_bigl => i; case Pi: (P i); rewrite // Qp. elim: {Q Qp}_.+1 {-2}Q (ltnSn #|Q|) => // n IHn Q. case: (pickP Q) => [j Qj | Q0 _]; last first. by rewrite !big_pred0 // => i; rewrite Q0 andbF. rewrite ltnS (cardD1x Qj) (bigD1 j) //; move/IHn=> {n IHn} <-. rewrite (bigID (fun i => p i == j)) => /=. apply: mon_eqv; apply: eqv_bigl => i. case: eqP => [-> | _] ; by rewrite ?(Qj) ?andbT ?andbF. by rewrite andbA. Qed.
imports: HB(structures) Coq(RelationClasses Morphisms Relation_Definitions) mathcomp(all_ssreflect)