proposition: Lemma ncvg_mono (u : nat -> R) : (forall x y, (x <= y)%N -> u x <= u y) -> exists2 l, (-oo < l)%E & ncvg u l.
proof: Proof. move=> mono_u; pose E := [set x | exists n, x = u n]%classic. have nzE: nonempty E by exists (u 0%N); exists 0%N. case: (pselect (has_sup E)); last first. move/has_supPn=> -/(_ nzE) h; exists +oo%E => //; elim/nbh_pinfW => M /=. case/(_ M): h=> x [K -> lt_MuK]; exists K=> n le_Kn; rewrite inE. by apply/(lt_le_trans lt_MuK)/mono_u. move=> supE; exists (sup E)%:E => //; first exact: ltNyr. elim/nbh_finW=>e /= gt0_e. case: (sup_adherent gt0_e supE)=> x [K ->] lt_uK. exists K=> n le_Kn; rewrite inE distrC ger0_norm ?subr_ge0. by move/ubP: (sup_upper_bound supE); apply; exists n. rewrite ltrBlDr addrC -ltrBlDr. by rewrite (lt_le_trans lt_uK) //; apply/mono_u. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology