proposition: Lemma big_setIDcond A B P F : \big[aop/idx]_(i in A | P i) F i = aop (\big[aop/idx]_(i in A :&: B | P i) F i) (\big[aop/idx]_(i in A :\: B | P i) F i).
proof: Proof. by rewrite !big_mkcondr; apply: big_setID. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)