proposition: Lemma cone0_of_cone0 (A: set E): cone0 (cone0_of A).
proof: Proof. move=>x [t /= _] [a [n [s [k [<- sA]]]]] <-. rewrite scaler_sumr; exists n, s, (fun i => mulRpos t (k i)); split => //. by apply congr_big=>// i _; apply /esym; apply scalerA. Qed.
imports: mathcomp(all_ssreflect all_algebra vector reals ereal classical_sets boolp Rstruct) infotheo(convex Reals_ext) preliminaries Reals