proposition: Lemma min_imperfectD S H : min_imperfect H -> S \in stabsets H -> ω(H :\: S) = ω(H).
proof: Proof. move=> min_imH stabS; apply/eqP; rewrite eqn_leq sub_omega ?subsetDl //=. have [K maxK disjK] := min_imperfect_maxclique min_imH stabS. rewrite -(card_maxclique maxK); apply: clique_bound. exact/maxcliquesW/maxclique_disjoint. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring) mathcomp(ssrint) mathcomp(all_algebra)