proposition: Lemma hull_setU (z : T) (X Y : {convex_set T}) : X !=set0 -> Y !=set0 -> hull (X `|` Y) z -> exists2 x, x \in X & exists2 y, y \in Y & exists p, z = x <| p |> y.
proof: Proof. move=> [dx ?] [dy ?] [n -[g [d [gT zg]]]]. suff [a] : exists2 a, a \in scaled_set X & exists2 b, b \in scaled_set Y & S1 z = addpt a b. have [-> _ [b bY]|a0 aX [b]] := eqVneq a Zero. rewrite add0pt => S1zy. exists dx; rewrite ?in_setE //; exists z; last by exists 0%:pr; rewrite conv0. by rewrite -(point_S1 z); apply: scaled_set_extract; rewrite S1zy. have [-> _|b0 bY] := eqVneq b Zero. rewrite addpt0 => S1zx. exists z; last by exists dy; rewrite ?in_setE //; exists 1%:pr; rewrite conv1. by rewrite -(point_S1 z); apply: scaled_set_extract; rewrite S1zx. rewrite addptE => -[_ zxy]. exists [point of a0]; first exact: (@scaled_set_extract _ a). exists [point of b0]; first exact: scaled_set_extract. by eexists; rewrite zxy. move/(congr1 (@S1 T)): zg; rewrite S1_Convn. rewrite (bigID (fun i => g i \in X)) /=. set b := \ssum_(i | _) _. set c := \ssum_(i | _) _. move=> zbc. exists b; first exact: ssum_scaled_set. exists c => //. apply: (@ssum_scaled_set _ [pred i | g i \notin X]) => i /=. move/asboolP; rewrite in_setE. by case: (gT (g i) (imageP _ I)). 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