proposition: Lemma conv_in_conv_set' p (X Y : set A) u : (X :<| p |>: Y) u -> exists x y, X x /\ Y y /\ u = x <| p |> y.
proof: Proof. by case=> x ?; rewrite conv_pt_setE=> -[] y ? <-; exists x, y. 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