fact: Definition coloring (G : sgraph) (P : {set {set G}}) (D : {set G}) := partition P D && [forall S in P, stable S].
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)