proposition: Lemma equiv_scal : forall {F : (T -> Prop) -> Prop} {FF : Filter F} (f g : T -> V) (c : K), (exists y : K, mult y c = one) -> is_equiv F f g -> is_equiv F (fun x => scal c (f x)) (fun x => scal c (g x)).
proof: Proof. intros F FF f g c [y Hc] H. apply domin_scal_l. by exists y. move => eps /=. cut (F (fun x => norm (scal c (minus (g x) (f x))) <= eps * norm (g x))). apply filter_imp => x. now rewrite scal_distr_l scal_opp_r. now apply domin_scal_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rbar Rcomplements Hierarchy