proposition: Lemma nondecreasing_cvgn_le u_ : nondecreasing_seq u_ -> cvgn u_ -> forall n, u_ n <= limn u_.
proof: Proof. move=> iu cu n; move: (@nonincreasing_cvgn_ge (- u_)). rewrite -nondecreasing_opp opprK => /(_ iu); rewrite is_cvgNE => /(_ cu n). by rewrite limN // lerNl opprK. 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