proposition: Lemma alphaP A : alpha_spec A α(A).
proof: Proof. rewrite /alpha_mem setE. have [/= S stabS maxS] := eq_bigmax_cond (fun A => #|A|) (stabsets_gt0 A). by rewrite maxS; apply: AlphaSpec; rewrite inE stabS -maxS -{2}[A]setE leqnn. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)