proposition: Lemma tuto_minsetP : forall P A, reflect ((P A) /\ (forall B, P B -> B \subset A -> B = A)) (minset P A).
proof: Proof. move=> P A; apply: (iffP forallP) => [minA | [PA minA] B]. split; first by have:= minA A; rewrite subxx eqxx /=; move/eqP. by move=> B PB sBA; have:= minA B; rewrite PB sBA /=; do 2!move/eqP. apply/implyP=> sBA; apply/eqP; apply/eqP/idP=> [-> //|]; move/minA; exact. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)