proposition: Lemma partition_big I (s : seq I) (J : finType) (P : pred I) (p : I -> J) (Q : pred J) F : (forall i, P i -> Q (p i)) -> \big[*%M/1]_(i <- s | P i) F i = \big[*%M/1]_(j : J | Q j) \big[*%M/1]_(i <- s | (P i) && (p i == j)) F i.
proof: Proof. move=> Qp; transitivity (\big[*%M/1]_(i <- s | P i && Q (p i)) F i). by apply: eq_bigl => i; case Pi: (P i); rewrite // Qp. have [n leQn] := ubnP #|Q|; elim: n => // n IHn in Q {Qp} leQn *. case: (pickP Q) => [j Qj | Q0]; last first. by rewrite !big_pred0 // => i; rewrite Q0 andbF. rewrite (bigD1 j) // -IHn; last by rewrite ltnS (cardD1x Qj) in leQn. rewrite (bigID (fun i => p i == j)); congr (_ * _); apply: eq_bigl => i. by case: eqP => [-> | _]; rewrite !(Qj, simpm). by rewrite andbA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)