proposition: Lemma addpt_scaled_set (X : {convex_set T}) x y : x \in scaled_set X -> y \in scaled_set X -> addpt x y \in scaled_set X.
proof: Proof. case: x => [p x|]; case: y => [q y|] //=; exact: mem_convex_set. 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