proposition: Lemma scalept_Scaled p q (x : A) : scalept p (q *: x) = scalept (p * q) (S1 x).
proof: Proof. rewrite /scalept /=. case: Rlt_dec => Hp; case: Rlt_dec => Hpq //. - congr (_ *: _); apply val_inj; by rewrite /= mulR1. - elim Hpq; by apply /mulR_gt0. - elim Hp; move/pmulR_lgt0: Hpq; exact. 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