proposition: Lemma equiv_le_2 {T} {K : AbsRing} {V : NormedModule K} F {FF : Filter F} (f g : T -> V) : is_equiv F f g -> F (fun x => norm (g x) <= 2 * norm (f x) /\ norm (f x) <= 2 * norm (g x)).
proof: Proof. intros H. apply filter_and. - move: (H (pos_div_2 (mkposreal _ Rlt_0_1))) => {H}. apply filter_imp => x /= H. apply Rle_trans with (1 := norm_triangle_inv _ _) in H. rewrite -Ropp_minus_distr Rabs_Ropp in H. apply Rabs_le_between' in H ; case: H => H _. field_simplify in H. rewrite ?Rdiv_1 in H. apply Rle_div_l in H. by rewrite Rmult_comm. by apply Rlt_0_2. - move: (H (mkposreal _ Rlt_0_1)) => {H}. apply filter_imp => x /= H. apply Rle_trans with (1 := norm_triangle_inv _ _) in H. rewrite -Ropp_minus_distr Rabs_Ropp in H. apply Rabs_le_between' in H ; case: H => _ H. field_simplify in H. by rewrite ?Rdiv_1 in H. Qed.
imports: Coq(Reals Psatz ssreflect) Rbar Rcomplements Hierarchy