proposition: Lemma preimage_cstM T (R : realFieldType) (x y : R) (f : T -> R) : x != 0 -> (cst x \* f) @^-1` [set y] = f @^-1` [set y / x].
proof: Proof. move=> x0; apply/seteqP; rewrite /preimage; split => [z/= <-|z/= ->]. by rewrite mulrAC divrr ?mul1r// unitfE. by rewrite mulrCA divrr ?mulr1// unitfE. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) signed reals ereal topology normedtype sequences real_interval esum measure lebesgue_measure numfun