proposition: Lemma chi0 : χ(@set0 G) = 0.
proof: Proof. apply/eqP; rewrite -leqn0; apply: leq_trans (color_bound empty_coloring) _. by rewrite cards0. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)