proposition: Lemma min_imperfect_maxclique H S : min_imperfect H -> S \in stabsets H -> exists2 K, K \in maxcliques H & [disjoint K & S].
proof: Proof. case/andP => impH /forall_inP perfH stabS. have [->|[x xS]] := set_0Vmem S. by case: omegaP (leqnn ω(H)) => K maxK _; exists K => //; rewrite disjoint_sym disjoints0. apply/exists_inP; apply: contraTT impH; rewrite negb_exists_in -ltnNge. move/forall_inP => /= maxDn. have [subSH ?] := stabsetsP _ _ stabS. apply: leq_ltn_trans (@chiD1 _ _ S _) _ => //. have/perfH/perfect_eq <- : H :\: S \proper H. apply/properP; split; [exact: subsetDl|exists x => //]. exact: (subsetP subSH). by rewrite !inE xS. by apply: omega_cut => K maxK; rewrite setIC setI_eq0 maxDn. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring) mathcomp(ssrint) mathcomp(all_algebra)