proposition: Lemma dominates_scale (A : finType) (Q P : A -> R) : P `<< Q -> forall k : R, k != 0%R -> P `<< [ffun a : A => k * Q a]%R.
proof: Proof. move=> PQ k k0; apply/dominatesP => a /eqP. by rewrite ffunE mulf_eq0 (negbTE k0)/= => /eqP/(dominatesE PQ). Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(lra ring Rstruct)