proposition: Lemma eseries_pinfty (R : realFieldType) (u_ : (\bar R)^nat) (P : pred nat) k : (forall n, P n -> u_ n != -oo) -> P k -> u_ k = +oo -> \sum_(i <oo | P i) u_ i = +oo.
proof: Proof. move=> uNy Pk uky; apply: lim_near_cst => //; near=> n. apply/eqP; rewrite big_mkord esum_eqy; last first. by move=> /= i Pi; rewrite uNy. apply/existsP. have kn : (k < n)%N by near: n; exists k.+1. by exists (Ordinal kn) => /=; rewrite uky eqxx andbT. Unshelve. all: by end_near. 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