proposition: Lemma hullI (X : set A) : hull (hull X) = hull X.
proof: Proof. rewrite predeqE => d; split. - move=> -[n [g [e [gX ->{d}]]]]. move: (hull_is_convex X). by rewrite is_convex_setP /is_convex_set_n => /asboolP/(_ _ g e gX). - by move/subset_hull. 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