proposition: Lemma Lovasz_tag_inj (S : {set Lovasz}) : stable S -> {in S &, injective tag}.
proof: Proof. move=> /stableP stabS [/= u x] [/= v y] uS vS uv; subst v; apply:eq_sigT => /=. apply: contraNeq (stabS _ _ uS vS) => xDy. by rewrite /edge_rel/=/LovaszRel/= eqxx -tag_eqE/tag_eq/= tagged_asE eqxx /=. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring)