proposition: Lemma Lovasz_stable_card (S : {set Lovasz}) : stable S -> #|tag @: S| = #|S|.
proof: Proof. move=> stabS. rewrite card_in_imset //. exact: Lovasz_tag_inj. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring)