proposition: Lemma conv_cset_is_convex (p : {prob R}) (X Y : {convex_set A}) : is_convex_set (conv_set p X Y).
proof: Proof. apply/asboolP=> u v q. case/conv_in_conv_set'=> x0 [] y0 [] ? [] ? ->. case/conv_in_conv_set'=> x1 [] y1 [] ? [] ? ->. by rewrite convACA; apply/conv_in_conv_set; [move/asboolP: (convex_setP X); apply | move/asboolP: (convex_setP Y); apply]. Qed.
imports: HB(structures) Reals mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets Rstruct reals) mathcomp(finmap) Reals_ext realType_ext classical_sets_ext ssrR fdist fsdist convex