proposition: Lemma esum_bigcupT J a : trivIset setT J -> (forall x, 0 <= a x) -> \esum_(i in \bigcup_(k in K) (J k)) a i = \esum_(i in K) \esum_(j in J i) a j.
proof: Proof. move=> tJ a0; rewrite esum_esum//; apply: reindex_esum => //; split. - by move=> [/= i j] [Ki Jij]; exists i. - move=> [/= i1 j1] [/= i2 j2]; rewrite ?inE/=. move=> [K1 J1] [K2 J2] j12; congr (_, _) => //. by apply: (@tJ i1 i2) => //; exists j1; split=> //; rewrite j12. - by move=> j [i Ki Jij]/=; exists (i, j). Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology sequences normedtype numfun