proposition: Lemma Lovasz_tag_clique (K : {set Lovasz}) : clique K -> clique (tag @: K).
proof: Proof. move => clK ? ? /imsetP[[x n] xnK ->] /imsetP[[y o] yoK ->] /= xDy. have := clK _ _ xnK yoK; rewrite -tag_eqE/tag_eq/= (negbTE xDy) => /(_ isT). by rewrite /edge_rel/=/LovaszRel/= (negbTE xDy). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring)