proposition: Lemma esumID (R : realType) (I : choiceType) (B : set I) (A : set I) (F : I -> \bar R) : (forall i, A i -> F i >= 0) -> \esum_(i in A) F i = (\esum_(i in A `&` B) F i) + (\esum_(i in A `&` ~` B) F i).
proof: Proof. move=> F0; rewrite !esum_mkcondr -esumD; do ?by move=> i /F0; case: ifP. by apply: eq_esum=> i; rewrite in_setC; case: ifP; rewrite /= (adde0, add0e). 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