proposition: Lemma nondecreasing_cvgr f : nondecreasing_fun f -> has_ubound (range f) -> f r @[r --> +oo] --> sup (range f).
proof: Proof. move=> ndf ubf; set M := sup (range f). have supf : has_sup (range f) by split => //; exists (f 0), 0. apply/cvgrPdist_le => _/posnumP[e]. have [p Mefp] : exists p, M - e%:num <= f p. have [_ -[p _] <- /ltW efp] := sup_adherent (gt0 e) supf. by exists p; rewrite efp. near=> n; have pn : p <= n by near: n; apply: nbhs_pinfty_ge; rewrite num_real. rewrite ler_distlC (le_trans Mefp (ndf _ _ _))//= (@le_trans _ _ M) ?lerDl//. by have /ubP := sup_upper_bound supf; apply; exists n. Unshelve. all: by end_near. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum finmap) mathcomp(matrix interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) ereal reals signed topology prodnormedzmodule normedtype derive sequences real_interval HB(structures)