proposition: Lemma cone0_of_sub_cone0_convex (A: set E) (B: {convex_set E}) : (A `<=` B -> cone0 B -> cone0_of A `<=` B)%classic.
proof: Proof. rewrite cone0_of_hullE=>AB Bcone x [t t0 [a aA <-]]. apply Bcone; exists t=>//; exists a=>//. by apply (hull_sub_convex AB). Qed.
imports: mathcomp(all_ssreflect all_algebra vector reals ereal classical_sets boolp Rstruct) infotheo(convex Reals_ext) preliminaries Reals