proposition: Lemma ncvg_mono_bnd (u : nat -> R) : (forall x y, (x <= y)%N -> u x <= u y) -> nbounded u -> exists l, ncvg u l%:E.
proof: Proof. case/ncvg_mono=> -[x||] // _ cu bdu; first by exists x. case/asboolP/nboundedP: bdu=> M gt0_M bdu. case/(_ (NPInf M)): cu => K /= /(_ K (leqnn _)). rewrite inE/= => /ltW /le_trans /(_ (ler_norm _)). by move/le_lt_trans/(_ (bdu _)); rewrite ltxx. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology