proposition: Lemma nondecreasing_cvgn (u_ : R ^nat) : nondecreasing_seq u_ -> has_ubound (range u_) -> u_ @ \oo --> sup (range u_).
proof: Proof. move=> leu u_ub; set M := sup (range u_). have su_ : has_sup (range u_) by split => //; exists (u_ 0%N), 0%N. apply/cvgrPdist_le => _/posnumP[e]. have [p Mu_p] : exists p, M - e%:num <= u_ p. have [_ -[p _] <- /ltW Mu_p] := sup_adherent (gt0 e) su_. by exists p; rewrite Mu_p. near=> n; have pn : (p <= n)%N by near: n; exact: nbhs_infty_ge. rewrite ler_distlC (le_trans Mu_p (leu _ _ _))//= (@le_trans _ _ M) ?lerDl//. by have /ubP := sup_upper_bound su_; apply; 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