proposition: Lemma tuto_minset_exists : forall P C, P C -> {A | minset P A & A \subset C}.
proof: Proof. move=> P C PC; have{PC}: exists A, P A && (A \subset C). by exists C; rewrite PC /=. case/ex_minset=> A; case/minsetP; case/andP=> PA sAC minA; exists A => //. apply/minsetP; split=> // B PB sBA; apply: minA => //. by rewrite PB (subset_trans sBA). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)