proposition: Lemma gtr0_cvgV0 f : (\near a, 0 < f a) -> f\^-1 @ a --> 0 <-> f @ a --> +oo.
proof: Proof. move=> f_gt0; split; last first. move=> /cvgryPgt cvg_f_oo; apply/cvgr0Pnorm_lt => _/posnumP[e]. near=> i; rewrite gtr0_norm ?invr_gt0//=; last by near: i. by rewrite -ltf_pV2 ?qualifE/= ?invr_gt0 ?invrK//=; near: i. move=> /cvgr0Pnorm_lt uB; apply/cvgryPgty. near=> M; near=> i; suff: `|(f i)^-1| < M^-1. by rewrite gtr0_norm ?ltf_pV2 ?qualifE ?invr_gt0//=; near: i. by near: i; apply: uB; rewrite ?invr_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