proposition: Lemma empty_coloring : coloring set0 (@set0 G).
proof: Proof. by rewrite /coloring partition_set0 eqxx; apply/forall_inP => S; rewrite inE. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)