proposition: Lemma ltr0_cvgV0 f : (\near a, 0 > f a) -> f\^-1 @ a --> 0 <-> f @ a --> -oo.
proof: Proof. move=> fL0; rewrite -cvgNP oppr0 (_ : - f\^-1 = (- f)\^-1); last first. by apply/funeqP => i; rewrite opprfctE/= invrN. by rewrite gtr0_cvgV0 ?cvgNry//; near do rewrite oppr_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