proposition: Lemma equiv_inv : forall {T} {F : (T -> Prop) -> Prop} {FF : Filter F} (f g : T -> R), F (fun x => g x <> 0) -> is_equiv F f g -> is_equiv F (fun x => / f x) (fun x => / g x).
proof: Proof. intros T F FF f g Hg H. have Hf : F (fun x => f x <> 0). generalize (filter_and _ _ Hg (H (pos_div_2 (mkposreal _ Rlt_0_1)))) => /=. apply filter_imp => x {Hg H} [Hg H]. case: (Req_dec (f x) 0) => Hf //. rewrite /minus /plus /opp /= Hf Ropp_0 Rplus_0_r in H. generalize (norm_ge_0 (g x)) (norm_eq_zero (g x)). rewrite /zero /=. lra. apply equiv_sym in H. move => eps. generalize (filter_and _ _ (filter_and _ _ Hf Hg) (H eps)). clear -FF. apply filter_imp. intros x [[Hf Hg] H]. rewrite /norm /= /abs /minus /plus /opp /=. replace (/ g x + - / f x) with ((f x - g x) / (f x * g x)). rewrite Rabs_div ?Rabs_Rinv ?Rabs_mult //. apply Rle_div_l. apply Rmult_lt_0_compat ; by apply Rabs_pos_lt. field_simplify ; rewrite ?Rdiv_1. by []. by apply Rabs_no_R0. by apply Rmult_integral_contrapositive_currified. field ; by split. Qed.
imports: Coq(Reals Psatz ssreflect) Rbar Rcomplements Hierarchy