proposition: Fact alpha_maxset S : stable S -> W S = alpha_w -> maxset stable S.
proof: Proof. move => stS alphaS; apply: maxweight_maxset => // A. rewrite -/W alphaS; exact: alpha_max. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)