proposition: Lemma Lovasz_tag_stable (S : {set Lovasz}) : stable S -> stable (tag @: S).
proof: Proof. move/stableP => stabS. apply/stableP => ? ? /imsetP[[/= u x] S1 ->] /imsetP[[/= v y] S2 ->]. have [<-|uDv] := eqVneq u v; first by rewrite sgP. by have := stabS _ _ S1 S2; rewrite {1}/edge_rel/=/LovaszRel/= (negbTE uDv). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring)