proposition: Lemma largest_maxset (p : pred {set T}) (A : {set T}) : largest p A -> maxset p A.
proof: Proof. move => [pA maxA]. apply/maxset_properP; split => // B /proper_card; rewrite ltnNge. exact/contraNN/maxA. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)