proposition: Proposition maxset_properP (p : pred {set T}) (D : {set T}) : reflect (p D /\ (forall F : {set T}, D \proper F -> ~~ p F)) (maxset p D).
proof: Proof. apply: (iffP maxsetP) => -[pD maxD]; split => // E. - rewrite properEneq => /andP [DnE DsubE]. apply: contra_neqN DnE => pE; exact/esym/maxD. - move => pE SsubE; apply: contraTeq pE => EnD; apply: maxD. by rewrite properEneq eq_sym EnD. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)