proposition: Lemma alpha0 : α(set0 : {set G}) = 0.
proof: Proof. by case: alphaP => S; rewrite !inE subset0 -!andbA => /and3P[/eqP ->]; rewrite cards0. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)