proposition: Proposition minset_properP (p : pred {set T}) (D : {set T}) : reflect (p D /\ (forall F : {set T}, F \proper D -> ~~ p F)) (minset p D).
proof: Proof. rewrite minmaxset; apply (iffP (maxset_properP _ _)). all: rewrite /= setCK => -[pD H]; split => // E. all: by rewrite properC ?setCK => /H; rewrite ?setCK. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)