proposition: Lemma cone0_of_hullE (A: set E): cone0_of A = [set (t : R_ringType) *: a | t in (@setT Rpos) & a in (hull A)]%classic.
proof: Proof. rewrite eqEsubset; split=>x. move=>[n [s [k [<- kA]]]]; set t := \sum_i (k i : R_ringType). have k0' (i : 'I_n.+1) : true -> 0 <= (k i : R_ringType) by move=> _; apply/ltW/RltP/Rpos_gt0. have: 0 <= t by apply sumr_ge0. rewrite le0r=>/orP; case. move=>/eqP /psumr_eq0P; move=> /(_ k0') /(_ ord0 Logic.eq_refl) k00; exfalso. by move:(Rpos_gt0 (k ord0))=>/RltP; rewrite k00 ltxx. move=>t0. have tk0: forall i, Rdefinitions.Rle (Rdefinitions.IZR BinNums.Z0) ([ffun i => t^-1 * k i] i). by move=>i; rewrite ffunE; apply/RleP/mulr_ge0; [ apply ltW; rewrite invr_gt0 | apply k0' ]. have tk1 : \sum_(i < n.+1) [ffun i => t^-1 * k i] i = 1. transitivity (\sum_(i < n.+1) t^-1 * k i). by apply congr_big=>// i _; rewrite ffunE. rewrite -mulr_sumr mulrC divff//. by move:t0; rewrite lt0r=>/andP[]. move:(t0)=>/RltP/ssrR.ltRP t0'; exists (Rpos.mk t0')=>//; exists (t^-1 *: \sum_i (k i : R_ringType) *: s i). exists n.+1, s, (@FDist.make _ (finfun (fun i=> t^-1 * k i)) tk0 tk1); split=> //. rewrite scaler_sumr avgnrE. apply congr_big=>// i _. by rewrite scalerA ffunE. by rewrite scalerA divff ?gt_eqF// scale1r. move=>[t /= _] [a [n [s [d [sA ->]]]]] <-. rewrite avgnrE scaler_sumr (@mathcomp_extra.bigID_idem _ _ _ _ _ _ _ _ (fun i=> 0 < d i)); [| apply addrA | apply addrC | apply addr0 ]. have ->: \sum_(i | true && ~~ (0 < d i)) (t : R_ringType) *: (d i *: s i) = \sum_(i | true && ~~ (0 < d i)) 0 *: 0. apply congr_big=>// i /andP [_]; rewrite lt0r negb_and negbK. move:(FDist.ge0 d i)=>/RleP->; rewrite orbF=>/eqP->. by rewrite 2!scale0r GRing.scaler0. rewrite -[\sum_(_ < _ | _) 0 *: 0]scaler_sumr scale0r addr0 -big_filter /=. remember [seq i <- index_enum [finType of 'I_n] | 0 < d i] as I; move: HeqI=>/esym HeqI. case: I HeqI=> [| i I] HeqI. exfalso; move: (FDist.f1 d) (oner_neq0 R_ringType); rewrite (@mathcomp_extra.bigID_idem _ _ _ _ _ _ _ _ (fun i=> 0 < d i)); [| apply addrA | apply addrC | apply addr0 ]. rewrite -big_filter HeqI big_nil/=. have ->: forall x, Rdefinitions.RbaseSymbolsImpl.Rplus Rdefinitions.RbaseSymbolsImpl.R0 x = 0+x by []. have ->: Rdefinitions.IZR (BinNums.Zpos 1%AC) = 1 by []. rewrite add0r=><- /eqP; apply. transitivity (\sum_(i < n | true && ~~ (0 < d i)) (0*0:R_ringType)). 2: by rewrite -mulr_sumr mul0r. by apply congr_big=>// i /= dile; move: (FDist.ge0 d i)=>/RleP; rewrite le0r mul0r=>/orP; case=> [ /eqP // | ]; move: dile=>/[swap]->. have: subseq (i::I) (index_enum [finType of 'I_n]) by rewrite -HeqI; apply filter_subseq. case: n s d sA i I HeqI=> [| n] s d sA i I HeqI. by inversion i. move=> /subseq_incl; move=> /(_ ord0); rewrite size_index_enum card_ord; move=> [f [fn flt]]. rewrite /cone0_of/=. exists (size I), (s \o (nth ord0 (i :: I))). simple refine (ex_intro _ _ _). move=>j; apply (mulRpos t). simple refine (Rpos.mk _). exact (d (nth ord0 (i :: I) j)). rewrite -HeqI. apply/ssrR.ltRP/RltP/(@nth_filter _ (fun i=> 0 < d i)). by rewrite HeqI. split. rewrite [in RHS]HeqI. rewrite -[in RHS](mask_true (s:=i :: I) (leqnn (size I).+1)) big_mask. apply congr_big=>// j. by rewrite nth_nseq; case:j=>/= j ->. move=>_ /=. by rewrite scalerA (tnth_nth ord0)/=. move=>+/= [j] _ <- =>_. by apply sA; eexists. Qed.
imports: mathcomp(all_ssreflect all_algebra vector reals ereal classical_sets boolp Rstruct) infotheo(convex Reals_ext) preliminaries Reals