proposition: Lemma real_cvgr_gt {T} {F : set_system T} {FF : Filter F} (f : T -> R) (y : R) : y \is Num.real -> f @ F --> y -> forall z, y > z -> \forall t \near F, f t \is Num.real -> f t > z.
proof: Proof. move=> yr Fy z zy; near=> x => fxr. rewrite -ltrN2 -(ltrD2l y) real_ltr_normlW// ?rpredB//. by near: x; apply: cvgr_dist_lt => //; rewrite subr_gt0. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule