proposition: Lemma oplus_conv_cset_is_convex (X Y : {convex_set A}) : is_convex_set (oplus_conv_set X Y).
proof: Proof. apply/asboolP=> u v p. case=> q _ [] xu Xxu; rewrite conv_pt_setE=> -[] yu Yyu <-. case=> r _ [] xv Xxv; rewrite conv_pt_setE=> -[] yv Yyv <-. apply (prob_trichotomy' p); rewrite ?conv0 ?conv1; [exact: conv_in_oplus_conv_set | exact: conv_in_oplus_conv_set | move=> op]. apply (prob_trichotomy' q) => [| |oq]. - rewrite conv0 (convC r) convA convC; apply conv_in_oplus_conv_set=> //. by move/asboolP: (convex_setP Y); apply. - rewrite conv1 convA; apply conv_in_oplus_conv_set=> //. by move/asboolP: (convex_setP X); apply. - apply (prob_trichotomy' r) => [| |or]. + rewrite conv0 -convA' ?oprob_neq1 //; apply conv_in_oplus_conv_set=> //. by move/asboolP: (convex_setP Y); apply. + rewrite conv1 convC convA; apply conv_in_oplus_conv_set=> //. by move/asboolP: (convex_setP X); apply. + case: (convACA' xu yu xv yv oq op or)=> q' [] p' [] r' ->. by apply conv_in_oplus_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