proposition: Lemma LovaszRel_irrefl : irreflexive LovaszRel.
proof: Proof. by move => [x i]; rewrite /LovaszRel/= !eqxx. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring)