proposition: Lemma hull2 (x y : A) : hull [set x; y]%classic = ((fun t => x <| t |> y) @` `[0%R, 1%R])%classic.
proof: Proof. rewrite eqEsubset; split; last first. move=> z [t /andP [t0 t1]] <-. rewrite bnd_simp in t0, t1. exists 2%N, (fun i => if i == 0 then x else y), (fun i => if i == 0 then t else `1- t). split; first by case; case=>//= n _; rewrite subr_ge0. - by rewrite big_ord_recl big_ord1/= addrCA subrr addr0. - by move=>a[]; case; case=>/= [|n] _ _ <-; [left|right]. - by rewrite big_ord_recl big_ord1. move=>z [n][g][d][d0 d1 gxy ->]. move:d1=>/esym/eqP; rewrite -subr_eq0 (bigID [pred i | g i == x])//= opprD. rewrite addrCA addrC subr_eq0=>/eqP/esym=>d1. exists (\sum_(i < n | g i == x) d i). rewrite inE; apply/andP; rewrite 2!bnd_simp {2}d1 -[(_<=1)%R]subr_ge0 opprB. by rewrite addrCA subrr addr0; split; apply sumr_ge0. rewrite/conv {2}d1 opprB addrCA subrr addr0 [RHS](bigID [pred i | g i == x])//=. congr (_ + _); rewrite scaler_suml; apply: congr_big=>// i. by move=> /eqP ->. have /gxy[->|->//] : range g (g i) by []. by rewrite eqxx. Qed.
imports: encompass conv mathcomp(all_ssreflect all_algebra vector reals normedtype) mathcomp(classical_sets boolp mathcomp_extra) counterclockwise mathcomp.algebra_tactics(ring) mathcomp.zify(zify)