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