proposition: Lemma nneseries_lim_ge (R : realType) (u_ : (\bar R)^nat) (P : pred nat) k : (forall n, P n -> 0 <= u_ n) -> \sum_(0 <= i < k | P i) u_ i <= \sum_(i <oo | P i) u_ i.
proof: Proof. move/ereal_nondecreasing_series/ereal_nondecreasing_cvgn/cvg_lim => -> //. by apply: ereal_sup_ub; exists k. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau