proposition: Lemma lt_lim u (M : R) : nondecreasing_seq u -> cvgn u -> M < limn u -> \forall n \near \oo, M <= u n.
proof: Proof. move=> ndu cu Ml; have [[n Mun]|/forallNP Mu] := pselect (exists n, M <= u n). near=> m; suff : u n <= u m by exact: le_trans. by near: m; exists n.+1 => // p q; apply/ndu/ltnW. have {}Mu : forall x, M > u x by move=> x; rewrite ltNge; apply/negP. have : limn u <= M by apply: limr_le => //; near=> m; apply/ltW/Mu. by move/(lt_le_trans Ml); rewrite ltxx. 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