proposition: Lemma esum_ge [R : realType] [T : choiceType] (I : set T) (a : T -> \bar R) x : (exists2 X : set T, fsets I X & x <= \sum_(i \in X) a i) -> x <= \esum_(i in I) a i.
proof: Proof. by move=> [X IX /le_trans->//]; apply: ereal_sup_ub => /=; exists X. 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