proposition: Lemma domin_scal_r : forall {F : (T -> Prop) -> Prop} {FF : Filter F} (f : T -> U) (g : T -> V) (c : Kv), is_domin F f g -> is_domin F f (fun x => scal c (g x)).
proof: Proof. intros F FF f g c H. case: (Req_dec (abs c) 0) => Hc. move => eps /=. apply filter_forall => x. eapply Rle_trans. apply @norm_scal. rewrite Hc Rmult_0_l. apply Rmult_le_pos. by apply Rlt_le, eps. by apply norm_ge_0. destruct (abs_ge_0 c) => //. clear Hc ; rename H0 into Hc. move => eps /=. assert (He : 0 < eps / abs c). apply Rdiv_lt_0_compat. by apply eps. by apply Hc. move: (H (mkposreal _ He)) => /= {H}. apply filter_imp => x H. eapply Rle_trans. apply @norm_scal. rewrite Rmult_comm ; apply Rle_div_r. by []. apply Rle_trans with (1 := H). apply Req_le ; rewrite /Rdiv ; ring. by apply sym_eq in H0. Qed.
imports: Coq(Reals Psatz ssreflect) Rbar Rcomplements Hierarchy