proposition: Lemma bigID_idem I r (a P : pred I) F : \big[op/x]_(i <- r | P i) F i = op (\big[op/x]_(i <- r | P i && a i) F i) (\big[op/x]_(i <- r | P i && ~~ a i) F i).
proof: Proof. rewrite -big_id_idem_AC big_mkcond_idem !(big_mkcond_idem _ _ F) -big_split_idem. by apply: eq_bigr => i; case: ifPn => //=; case: ifPn; rewrite // opC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)