proposition: Lemma partition_disjoint_bigcup (F : I -> {set T}) E : (forall i j, i != j -> [disjoint F i & F j]) -> \big[op/idx]_(x in \bigcup_i F i) E x = \big[op/idx]_i \big[op/idx]_(x in F i) E x.
proof: Proof. move=> disjF; pose P := [set F i | i in I & F i != set0]. have trivP: trivIset P. apply/trivIsetP=> _ _ /imsetP[i _ ->] /imsetP[j _ ->] neqFij. by apply: disjF; apply: contraNneq neqFij => ->. have ->: \bigcup_i F i = cover P. apply/esym; rewrite cover_imset big_mkcond; apply: eq_bigr => i _. by rewrite inE; case: eqP. rewrite big_trivIset // /rhs big_imset => [|i j _ /setIdP[_ notFj0] eqFij]. rewrite big_mkcond; apply: eq_bigr => i _; rewrite inE. by case: eqP => //= ->; rewrite big_set0. by apply: contraNeq (disjF _ _) _; rewrite -setI_eq0 eqFij setIid. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)