proposition: Lemma card_maxstabset K H : K \in maxstabsets H -> #|K| = α(H).
proof: Proof. rewrite inE => /andP[stabS ltS]; apply/eqP; rewrite eqn_leq ltS andbT. exact: stabset_bound. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)