proposition: Lemma ex_minset P : (exists A, P A) -> {A | minset P A}.
proof: Proof. move=> exP; pose pS n := [pred B | P B & #|B| == n]. pose p n := ~~ pred0b (pS n); have{exP}: exists n, p n. by case: exP => A PA; exists #|A|; apply/existsP; exists A; rewrite /= PA /=. case/ex_minnP=> n /pred0P; case: (pickP (pS n)) => // A /andP[PA] /eqP <-{n} _. move=> minA; exists A => //; apply/minsetP; split=> // B PB sBA; apply/eqP. by rewrite eqEcard sBA minA //; apply/pred0Pn; exists B; rewrite /= PB /=. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)