proposition: Lemma nondecreasing_dvgn_lt (u_ : R ^nat) : nondecreasing_seq u_ -> ~ cvgn u_ -> u_ @ \oo --> +oo.
proof: Proof. move=> nu du; apply: contrapT => /cvgryPge/existsNP[l lu]; apply: du. apply: nondecreasing_is_cvgn => //; exists l => _ [n _ <-]. rewrite leNgt; apply/negP => lun; apply: lu; near=> m. by rewrite (le_trans (ltW lun)) //; apply: nu; near: m; exists n. 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