proposition: Lemma nonincreasing_cvgn_ge u_ : nonincreasing_seq u_ -> cvgn u_ -> forall n, limn u_ <= u_ n.
proof: Proof. move=> du ul p; rewrite leNgt; apply/negP => up0. move/cvgrPdist_lt : ul => /(_ `|u_ p - limn u_|%R). rewrite {1}ltr0_norm ?subr_lt0 // opprB subr_gt0 => /(_ up0) ul. near \oo => N. have /du uNp : (p <= N)%nat by near: N; rewrite nearE; exists p. have : `|limn u_ - u_ N| >= `|u_ p - limn u_|%R. rewrite ltr0_norm // ?subr_lt0 // opprB distrC. rewrite (@le_trans _ _ (limn u_ - u_ N)) // ?lerB //. rewrite (_ : `| _ | = `|u_ N - limn u_|%R) // ler0_norm // ?opprB //. by rewrite subr_le0 (le_trans _ (ltW up0)). rewrite leNgt => /negP; apply; by near: N. 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