proposition: Lemma compre_scale T (h : R -> \bar R) (f : T -> R) k : {morph h : x y / (x * y)%R >-> (x * y)%E} -> h \o (k \o* f) = (fun t => h k * h (f t))%E.
proof: Proof. by move=> mf; apply/funext => t /=; rewrite mf; rewrite muleC. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(fsbigop cardinality set_interval) reals signed topology constructive_ereal