proposition: Lemma domin_mult_l : forall {T} {F : (T -> Prop) -> Prop} {FF : Filter F} (f g h : T -> R), is_domin F f g -> is_domin F (fun x => h x * f x) (fun x => h x * g x).
proof: Proof. intros T F FF f g h H eps. generalize (domin_mult_r f g h H eps). apply filter_imp => x. by rewrite ?(Rmult_comm (h x)). Qed.
imports: Coq(Reals Psatz ssreflect) Rbar Rcomplements Hierarchy