proposition: Lemma hull_is_convex (Z : set A) : is_convex_set (hull Z).
proof: Proof. apply/asboolP => x y p [n [g [d [gX ->{x}]]]] [m [h [e [hX ->{y}]]]]. exists (n + m). exists [ffun i => match fintype.split i with inl a => g a | inr a => h a end]. exists (fdist_add d e p). split. move=> a -[i _]; rewrite ffunE. by case: splitP => j _ <-; [apply gX; exists j | apply hX; exists j]. by rewrite fdist_convn_add; congr (_ <| _ |> _); apply eq_Convn => i //=; rewrite ffunE (split_lshift,split_rshift). 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