proposition: Lemma scaler_scalept r x : (0 <= r -> scaler (scalept r x) = r *: scaler x)%coqR.
proof: Proof. case: x => [q y|r0]; last first. by rewrite scalept0// scaler0 !GRing.scaler0. case=> r0. by rewrite scalept_gt0 /= scalerA. by rewrite -r0 scale0pt scale0r. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets Rstruct) mathcomp(ssrnum ereal) mathcomp(lra Rstruct reals) Reals ssrR Reals_ext Ranalysis_ext ssr_ext ssralg_ext logb realType_ext fdist