proposition: Lemma eq_esum [R : realType] [T : choiceType] (I : set T) (a b : T -> \bar R) : (forall i, I i -> a i = b i) -> \esum_(i in I) a i = \esum_(i in I) b i.
proof: Proof. by move=> e; apply/eqP; rewrite eq_le !le_esum// => i Ii; rewrite e. 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