proposition: Lemma le_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. move=> le_ab; rewrite ub_ereal_sup => //= _ [X [finX XI]] <-; rewrite esum_ge//. by exists X => //; apply: lee_fsum => // t /XI /le_ab. 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