proposition: Lemma perfect0 : perfect (set0 : {set G}).
proof: Proof. by apply/forall_inP => A; rewrite subset0 => /eqP->; rewrite omega0 chi0. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring)