fact: Definition LovaszRel (u v : Σ x : G, 'I_(m x)) := if tag u == tag v then u != v else tag u -- tag v.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring)