proposition: Lemma nondecreasing_at_right_is_cvgr f a : (\forall x \near a^'+, {in `]a, x[ &, nondecreasing_fun f}) -> (\forall x \near a^'+, has_lbound (f @` `]a, x[)) -> cvg (f x @[x --> a ^'+]).
proof: Proof. move=> ndf lbf; apply/cvg_ex; near a^'+ => b. by eexists; apply: (@nondecreasing_at_right_cvgr _ _ (BLeft b)); [rewrite bnd_simp|near: b..]. 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)