proposition: Lemma near_nonincreasing_is_cvgn (u_ : R ^nat) (m : R) : {near \oo, nonincreasing_seq u_} -> (\forall n \near \oo, m <= u_ n) -> cvgn u_.
proof: Proof. move=> u_ni u_m. rewrite -(opprK u_); apply: is_cvgN; apply/(@near_nondecreasing_is_cvgn _ (- m)). - by apply: filterS u_ni => x u_x y xy; rewrite lerNl opprK u_x. - by apply: filterS u_m => x u_x; rewrite 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