proposition: Lemma esum_ge0 (S : set T) a : (forall x, S x -> 0 <= a x) -> 0 <= \esum_(i in S) a i.
proof: Proof. move=> a0; apply: ereal_sup_ub. by exists set0; [exact: fsets_set0|rewrite fsbig_set0]. 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