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