proposition: Lemma nnseries_is_cvg {R : realType} (u : nat -> R) : (forall i, 0 <= u i)%R -> \sum_(k <oo) (u k)%:E < +oo -> cvgn (series u).
proof: Proof. move=> ? ?; apply: nondecreasing_is_cvgn. move=> m n mn; rewrite /series/=. rewrite -(subnKC mn) {2}/index_iota subn0 iotaD big_cat/=. by rewrite add0n -{2}(subn0 m) -/(index_iota _ _) lerDl sumr_ge0. exists (fine (\sum_(k <oo) (u k)%:E)). rewrite /ubound/= => _ [n _ <-]; rewrite -lee_fin fineK//; last first. rewrite fin_num_abs gee0_abs//; apply: nneseries_ge0 => // i _. by rewrite lee_fin. by rewrite -sumEFin; apply: nneseries_lim_ge => i _; rewrite lee_fin. 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