proposition: Lemma gee_cvgy f g : (\near a, f a <= g a) -> f @ a --> +oo -> g @ a --> +oo.
proof: Proof. move=> uv /cvgeyPge uecvg; apply/cvgeyPge => A. by near=> x do rewrite (le_trans _ (near uv x _))//. Unshelve. all: 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