proposition: Lemma maxsetP P A : reflect ((P A) /\ (forall B, P B -> A \subset B -> B = A)) (maxset P A).
proof: Proof. apply: (iffP minsetP); rewrite ?setCK unlock_with => [] [PA minA]. by split=> // B PB sAB; rewrite -[B]setCK [~: B]minA (setCK, setCS). by split=> // B PB' sBA'; rewrite -(minA _ PB') -1?setCS setCK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)