proposition: Lemma hullU_strr X Y : hull (X `|` hull Y) = hull (X `|` Y).
proof: Proof. apply/hull_eqEsubset => a. - case; first by move=> ?; apply/subset_hull; left. case=> n [d [g [H0 H1]]]; exists n, d, g; split => //. apply (subset_trans H0) => ? ?; by right. - case => [?|?]; first by apply/subset_hull; left. apply/subset_hull; right. exact/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