proposition: Lemma stabset_bound S A : S \in stabsets A -> #|S| <= α(A).
proof: Proof. by move => stabS; apply: bigmax_sup (leqnn _); rewrite setE. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)