proposition: Lemma domin_mult_r : forall {T} {F : (T -> Prop) -> Prop} {FF : Filter F} (f g h : T -> R), is_domin F f g -> is_domin F (fun x => f x * h x) (fun x => g x * h x).
proof: Proof. intros T F FF f g h H eps. move: (H eps) => {H}. apply filter_imp => x H1. rewrite /norm /= /abs /= ?Rabs_mult. rewrite -Rmult_assoc. apply Rmult_le_compat_r. by apply Rabs_pos. by apply H1. Qed.
imports: Coq(Reals Psatz ssreflect) Rbar Rcomplements Hierarchy