proposition: Lemma hull_sub_convex (X : set A)(Y : {convex_set A}) : (X `<=` Y -> hull X `<=` Y)%classic.
proof: Proof. move=> XY x [n [g [d [gX ->]]]]. have := convex_setP Y; rewrite is_convex_setP /is_convex_set_n. by move=> /asboolP/(_ _ g d (subset_trans gX XY)). 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