proposition: Lemma dominates_cscaler d (T : measurableType d) (R : realType) (nu : {charge set T -> \bar R}) (mu : set T -> \bar R) (c : R) : c != 0%R -> mu `<< nu -> mu `<< cscale c nu.
proof: Proof. move=> /negbTE c0 munu E mE /eqP; rewrite /cscale mule_eq0 eqe c0/=. by move=> /eqP/munu; exact. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets cardinality) mathcomp(functions fsbigop set_interval) HB(structures) reals ereal signed topology numfun normedtype sequences esum measure realfun lebesgue_measure lebesgue_integral