proposition: Lemma nneseries_pinfty (R : realType) (u_ : (\bar R)^nat) (P : pred nat) k : (forall n, P n -> 0 <= u_ n) -> P k -> u_ k = +oo -> \sum_(i <oo | P i) u_ i = +oo.
proof: Proof. move=> u_ge0 Pk ukoo; apply: (eseries_pinfty _ Pk ukoo) => // n Pn. by rewrite gt_eqF// (lt_le_trans _ (u_ge0 _ Pn)). 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