proposition: Lemma subset_hull X : X `<=` hull X.
proof: Proof. move=> x xX; rewrite /hull; exists 1, (fun=> x), (fdist1 ord0). split => [d [i _ <-] //|]; by rewrite ConvnI1E. 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