proposition: Lemma big_fsetIDcond (B : pred I) (A : {fset I}) (P : pred I) (F : I -> R) : \big[op/idx]_(i <- A | P i) F i = op (\big[op/idx]_(i <- [fset x in A | B x] | P i) F i) (\big[op/idx]_(i <- [fset x in A | ~~ B x] | P i) F i).
proof: Proof. by rewrite big_mkcond (big_fsetID B) // -!big_mkcond. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)