proposition: Lemma perfectPn H : reflect (exists2 A : {set G}, A \subset H & min_imperfect A) (~~ perfect H).
proof: Proof. apply: (iffP forall_inPn) => -[A]; last first. move=> subAH /andP[lt_ω_α /forall_inP perfS]. exists A => //. by rewrite eqn_leq negb_and -!ltnNge lt_ω_α orbT. rewrite unfold_in => subAH neq_ω_α. exists [arg min_(B < A | (B \subset A) && (ω(B) != χ(B))) #|B|]. case: arg_minnP; first by rewrite subxx. move=> B /andP[subBA _ _]; exact: subset_trans subAH. case: arg_minnP; first by rewrite subxx. move=> B /andP[subBA imB] minB; rewrite eqn_leq omega_leq_chi /= -ltnNge in imB. rewrite /min_imperfect_mem imB; apply/forall_inP => C subCB. apply/forall_inP => D subDC. have propDB : D \proper B by apply: sub_proper_trans subCB. move: (proper_card propDB). apply: contraTT; rewrite -ltnNge ltnS. by move: (minB D); rewrite (subset_trans _ subBA) // proper_sub. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring) mathcomp(ssrint) mathcomp(all_algebra)