proposition: Lemma existb_sig (A : finType) (P : {pred A}) : [exists x, P x] -> {x | P x}.
proof: Proof. move=> He. suff: [set x | P x] != finset.set0. case: (set_0Vmem [set x | P x]) => /=[/eqP -> // | [x]]. rewrite inE => Hx _; by exists x. case/existsP: He => x Px. apply/eqP => /setP/(_ x). by rewrite inE Px inE. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets) Reals mathcomp(Rstruct reals) ssrR Reals_ext realType_ext Ranalysis_ext ssr_ext ssralg_ext fdist jfdist_cond fsdist convex