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