proposition: Lemma perfectEstrong (U H : {set G}) (v : G) : perfect U -> H \subset U -> v \in H -> exists S, [/\ stable S, S \subset H, v \in S & [forall K in maxcliques H, S :&: K != set0]].
proof: Proof. move=> perfG subHU vH. have/eqP := forall_inP perfG _ subHU. case: chiP => P /andP[partP stabP] optP E. pose S := pblock P v. have vP : v \in cover P by rewrite (cover_partition partP) vH. have SP : S \in P by rewrite pblock_mem // vP. have SH : S \subset H by rewrite -(cover_partition partP); apply: bigcup_sup SP. exists S; rewrite SH mem_pblock vP (forall_inP stabP) //; split => //. apply: contra_eqT (E) => /forall_inPn/= [K maxK]; rewrite negbK setI_eq0 => disjK. have colP' : coloring (P :\ S) (H :\: S) by apply: coloringD1 => //; apply/andP;split. rewrite eqn_leq negb_and -!ltnNge; apply/orP;right. have ωH : ω(H) <= ω(H :\: S). { rewrite -(card_maxclique maxK) clique_bound //. move: maxK; rewrite !inE -andbA => /and3P[K1 -> _]. by rewrite subsetD K1 disjoint_sym disjK. } apply: leq_ltn_trans ωH _. apply: leq_ltn_trans (omega_leq_chi _) _. by apply: leq_ltn_trans (color_bound colP') _; rewrite [#|P|](cardsD1 S) SP. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring)