fact: Definition chi_mem (G : sgraph) (A : mem_pred G) := #|[arg min_(P < trivial_coloring [set x in A] | coloring P [set x in A]) #|P|]|.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)