proposition: Lemma perfect_eq (G : sgraph) (A : {set G}) : perfect A -> ω(A) = χ(A).
proof: Proof. by move/forall_inP => /(_ A (subxx A)) => /eqP. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring) mathcomp(ssrint)