proposition: Lemma LovaszRel_sym : symmetric LovaszRel.
proof: Proof. by move=> u v; rewrite /LovaszRel [tag u == _]eq_sym [u == v]eq_sym sgP. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring)