proposition: Lemma bigU_idem (I : finType) (A B : pred I) F : [disjoint A & B] -> \big[op/x]_(i in [predU A & B]) F i = op (\big[op/x]_(i in A) F i) (\big[op/x]_(i in B) F i).
proof: Proof. move=> dAB; rewrite (bigID_idem (mem A)). congr (op : _ -> _); apply: eq_bigl => i; first by rewrite orbK. by have:= pred0P dAB i; rewrite andbC /= !inE; case: (i \in A). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)