proposition: Lemma dvg_nseries (u : nat^nat) : ~ cvgn (nseries u) -> nseries u @ \oo --> \oo.
proof: Proof. move=> du; apply: contrapT => /cvgnyPgt/existsNP[l lu]; apply: du. apply: nat_nondecreasing_is_cvg => //; first exact: le_nseries. exists l => _ [n _ <-]; rewrite leNgt; apply/negP => lun; apply: lu. by near do rewrite (leq_trans lun) ?le_nseries//; apply: nbhs_infty_ge. 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