proposition: Lemma alpha_Lovasz : α([set: Lovasz]) <= α([set: G]).
proof: Proof. case: alphaP => S /maxstabset_stable => stabS. rewrite -(Lovasz_stable_card stabS); apply: stabset_bound. by rewrite inE subsetT Lovasz_tag_stable. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring)