proposition: Lemma tuto_ex_minset : forall P, (exists A, P A) -> {A | minset P A}.
proof: Proof. move=> P 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; move/pred0P; case: (pickP (pS n)) => // A. case/andP=> PA; move/eqP=> <- {n} _ minA; exists A => //. apply/minsetP; split=> // B PB sBA; apply/eqP; rewrite eqEcard sBA. by apply: minA; apply/pred0Pn; exists B; rewrite /= PB /=. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)