proposition: Lemma cone0_convex (A: set E): cone0 A -> (is_convex_set A <-> ([set a+b | a in A & b in A] `<=` A)%classic).
proof: Proof. have ne20: (2 : R_ringType) != 0 by rewrite intr_eq0. have /RltP/ssrR.ltRP gt20: (0 : R_ringType) < 2 by rewrite ltr0z. move=>Acone; split=>Aconv. move=>x [u uA] [v vA] <-. have uA2: A (2 *: u) by apply Acone; exists (Rpos.mk gt20)=>//; exists u. have vA2: A (2 *: v) by apply Acone; exists (Rpos.mk gt20)=>//; exists v. move:Aconv=>/asboolP/(_ _ _ (probinvn 1) uA2 vA2); congr A. by rewrite/conv/= probinvn1 onem_half 2!scalerA mulrC divff// 2!scale1r. apply/asboolP. move=>x y t xA yA. move:(prob_ge0 t)=>/RleP; rewrite le0r=>/orP; case. by rewrite/conv/= =>/eqP ->; rewrite scale0r add0r onem0 scale1r. move=>/RltP/ssrR.ltRP t0; move: (prob_le1 t)=>/RleP; rewrite -subr_ge0 le0r=>/orP; case. by rewrite subr_eq0 /conv/= =>/eqP <-; rewrite onem1 scale0r addr0 scale1r. move=>/RltP/ssrR.ltRP t1; apply Aconv; exists ((t : R_ringType) *: x); [| exists ((onem t) *: y) ]=>//; apply Acone. by exists (Rpos.mk t0)=>//; exists x. by exists (Rpos.mk t1)=>//; exists y. Qed.
imports: mathcomp(all_ssreflect all_algebra vector reals ereal classical_sets boolp Rstruct) infotheo(convex Reals_ext) preliminaries Reals