fact: Definition perfect_mem (G : sgraph) (U : mem_pred G) := [forall (A : {set G} | A \subset U), ω(A) == χ(A)].
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring)