proposition: Lemma conv0_pt_set x (Y : set A) : x <| 0%:pr |>: Y = Y.
proof: Proof. rewrite eqEsubset; split => u; rewrite conv_pt_setE. - by case=> y Yy <-; rewrite conv0. - by move=> Yu; exists u=> //; rewrite conv0. 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