proposition: Lemma bigU (I : finType) (A B : pred I) F : [disjoint A & B] -> \big[*%M/1]_(i in [predU A & B]) F i = (\big[*%M/1]_(i in A) F i) * (\big[*%M/1]_(i in B) F i).
proof: Proof. exact/bigU_idem/mul1m. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)