proposition: Lemma scalept_weight p (x : scaled A) : 0 <= p -> weight (scalept p x) = p * weight x.
proof: Proof. case=> [p0|<-]; last by rewrite scale0pt mul0R. case: x => [r y|]; first by rewrite /= /scalept/=; case: Rlt_dec. by rewrite scalept0 ?mulR0//; exact/ltRW. 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