proposition: Lemma scalept_conv (T : convType) (x y : R) (s : scaled T) (p : {prob R}): 0 <= x -> 0 <= y -> scalept (x <|p|> y) s = scalept x s <|p|> scalept y s.
proof: Proof. move=> x0 y0; rewrite scaleptDl; [|exact/mulR_ge0|exact/mulR_ge0]. by rewrite convptE !scaleptA. 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