proposition: Lemma minweight_minset p A : p A -> (forall B, p B -> W A <= W B) -> minset p A.
proof: Proof. move => pA minA; apply/minset_properP; split => // B /ltnwset; rewrite ltnNge. exact/contraNN/minA. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)