proposition: Theorem weak_perfect (G : sgraph) : perfect G -> perfect (compl G).
proof: Proof. rewrite -!perfectT => perfG ; apply: perfectIweak => H _ H0. suff [K [clK subKH maxK]] : exists (K : {set G}), [/\ cliqueb K, K \subset H & [forall S in @maxstabsets G H, K :&: S != set0]]. { by exists K; rewrite stable_compl clK subKH maxcliques_compl. } change {set G} in H; have {H0} [x xH] := set0Pn _ H0. have perfH : perfect (induced H). by rewrite perfect_induced; apply: sub_perfect perfG. have [K clK /forall_inP cutK] := @weak_perfect_aux (induced H) (Sub x xH) perfH. pose i := induced_isubgraph H. exists (val @: K). rewrite -cliqueb_induced clK sub_induced; split => //. apply/forall_inP => S /maxstabset_to_induced /cutK. case/set0Pn => z; rewrite !inE => /andP[zK zS]; apply/set0Pn; exists (i z). by rewrite inE zS imset_f. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring) mathcomp(ssrint)