proposition: Lemma alpha_eq0 H : (α(H) == 0) = (H == set0).
proof: Proof. apply/idP/idP => [|/eqP->]; last by rewrite alpha0. apply: contraTT => /set0Pn[x xH]; rewrite -lt0n -(cards1 x). by apply: stabset_bound; rewrite !inE stable1 sub1set xH. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)