proposition: Lemma perfectIweak (U : {set G}) : (forall H : {set G}, H \subset U -> H != set0 -> exists S : {set G}, [/\ stable S, S \subset H & [forall K in maxcliques H, S :&: K != set0]]) -> perfect U.
proof: Proof. move=> ex_stable; apply/forall_inP => /= H. elim/card_ind : H => H IH subHU. have [->|HD0] := eqVneq H set0; first by rewrite omega0 chi0. have [S [stabS subSH /forall_inP cutS]] := ex_stable H subHU HD0. rewrite eqn_leq omega_leq_chi /=. case: {-}_ /(omegaP H) => /= K maxK. have cardHS : #|H :\: S| < #|H|. { rewrite cardsDS // ltn_subrL; move/set0Pn : (cutS K maxK) => [x /setIP[xS _]]. by apply/andP; split; apply/card_gt0P; exists x => //; apply: (subsetP subSH). } apply: leq_trans (chiD1 _ stabS) _. rewrite -(eqP (IH _ _ _)) //; first exact: omega_cut. by rewrite subDset subsetU // subHU orbT. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring)