proposition: Lemma bigU : forall (I : finType) (P Q : pred I) F, [disjoint P & Q] -> \big[*%M/1]_(i \in [predU P & Q]) F i === (\big[*%M/1]_(i \in P) F i) * (\big[*%M/1]_(i \in Q) F i).
proof: Proof. move=> I P Q F dAB; rewrite -> (bigID _ (mem P)); apply op_morph. by apply eq_bigl; rewrite /mem // /in_mem; move=> i //=; rewrite orbK. by apply eq_bigl; move=> i //=; have:= pred0P dAB i; rewrite andbC /= !inE; case: (i \in P). Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops