proposition: Lemma domin_inv : forall {T} {F : (T -> Prop) -> Prop} {FF : Filter F} (f g : T -> R), F (fun x => g x <> 0) -> is_domin F f g -> is_domin F (fun x => / g x) (fun x => / f x).
proof: Proof. intros T F FF f g Hg H eps. have Hf : F (fun x => f x <> 0). generalize (filter_and _ _ Hg (H (mkposreal _ Rlt_0_1))) => /=. apply filter_imp => x {Hg H} [Hg H]. case: (Req_dec (f x) 0) => Hf. rewrite /norm /= /abs /= Hf Rabs_R0 Rmult_0_r in H. apply Rlt_not_le in H. move => _ ; apply H. by apply Rabs_pos_lt. by []. generalize (filter_and _ _ (H eps) (filter_and _ _ Hf Hg)) => {H Hf Hg}. apply filter_imp => x [H [Hf Hg]]. rewrite /norm /= /abs /= ?Rabs_Rinv => //. replace (/ Rabs (f x)) with (Rabs (g x) / (Rabs (f x) * Rabs (g x))) by (field ; split ; by apply Rabs_no_R0). replace (eps * / Rabs (g x)) with (eps * Rabs (f x) / (Rabs (f x) * Rabs (g x))) by (field ; split ; by apply Rabs_no_R0). apply Rmult_le_compat_r. apply Rlt_le, Rinv_0_lt_compat, Rmult_lt_0_compat ; apply Rabs_pos_lt => //. by apply H. Qed.
imports: Coq(Reals Psatz ssreflect) Rbar Rcomplements Hierarchy