proposition: Lemma near_nondecreasing_is_cvgn (u_ : R ^nat) (M : R) : {near \oo, nondecreasing_seq u_} -> (\forall n \near \oo, u_ n <= M) -> cvgn u_.
proof: Proof. move=> [k _ u_nd] [k' _ u_M]. suff : cvgn [sequence u_ (n + maxn k k')%N]_n. by case/cvg_ex => /= l; rewrite cvg_shiftn => ul; apply/cvg_ex; exists l. apply: nondecreasing_is_cvgn; [move=> /= m n mn|exists M => _ [n _ <-]]. by rewrite u_nd ?leq_add2r//= (leq_trans (leq_maxl _ _) (leq_addl _ _)). by rewrite u_M //= (leq_trans (leq_maxr _ _) (leq_addl _ _)). 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