proposition: Lemma segment_hull (x y : A) : segment x y = hull [set x; y].
proof: Proof. rewrite eqEsubset; split. by have := hull_is_convex [set x; y] => /is_convex_segmentP/(_ x y); apply; apply subset_hull; [left | right]. pose h := convex_set_of_segment x y. by have := @hull_sub_convex [set x; y] h; apply => z -[] ->; [exact: segmentL|exact: segmentR]. 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