proposition: Lemma big_union (X1 X2 : {set A}) f : [disjoint X2 & X1] -> \big[M/idx]_(a | a \in X1 :|: X2) f a = M (\big[M/idx]_(a | a \in X1) f a) (\big[M/idx]_(a | a \in X2) f a).
proof: Proof. move=> Hdisj. rewrite (@big_setID _ _ _ _ _ X1) /= setUK setDUl setDv set0U. suff : X2 :\: X1 = X2 by move=> ->. by apply/setDidPl. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) logb ssr_ext ssralg_ext