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