proposition: Lemma partition_big : forall (I J : finType) (P : pred I) p (Q : pred J) F, (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=> I J P p Q F Qp; transitivity (\big[*%M/1]_(i | P i && Q (p i)) F i). by apply eq_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=> //; try reflexivity; move=> i//=; rewrite Q0 andbF. rewrite ltnS (cardD1x Qj); rewrite -> (bigD1 (j:=j))=> //; move/IHn=> {n IHn} Heq; rewrite <- Heq. rewrite -> (bigID _ (fun i => p i == j)); apply op_morph. by apply eq_bigl=> i//=; case: eqP => [-> | _]; rewrite ?Qj //= andbC //= andbC //=. by apply eq_bigl=> i//=; rewrite andbA. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops