proposition: Theorem Hajnal A : reflect (forall B, B \subset A -> #|B| <= α(B) * ω(B)) (perfect A).
proof: Proof. apply introP => [perfA B subBA|]. { rewrite perfect_eq ?(sub_perfect subBA) // mulnC. have [P /coloring_stabsetP [partP stabP] _] := chiP. rewrite -{1}(cover_partition partP) /cover. have/eqP <- : trivIset P by case/and3P : partP. rewrite -sum_nat_const; apply: leq_sum => C /stabP; exact: stabset_bound. } case/perfectPn => H subHA minH => /(_ H subHA); apply/negP; rewrite -ltnNge. have {A subHA} := min_imperfect_stabsets_cliques minH. set a := α(H); set w := ω(H); set k := (a * w).+1; set n := #|H|. move => [S] [K] [stabS maxK _ disjKS capKS]. pose x (i : 'I_n) : G := enum_val i. pose MS := (\matrix_(i < n, j < k) (x i \in S j : int))%R. pose MK := (\matrix_(i < n, j < k) (x i \in K j : int))%R. suff: (MS^T *m MK = \matrix_(i < k,j < k) (i != j : int))%R. { apply: rank_argument. by rewrite /k ltnS muln_gt0 !lt0n alpha_eq0 omega_eq0 min_imperfect_neq0. } apply/matrixP => i j; rewrite !mxE. under eq_bigr => z do rewrite !mxE mulb -in_setI /=. have [<- {j}|iDj] /= := eqVneq i j. - under eq_bigr => z do rewrite setIC (disjoint_setI0 (disjKS i)) inE /=. by rewrite GRing.sumr_const GRing.mul0rn. - rewrite eq_sym in iDj. move/capKS/mem_card1 : (iDj) => [v vP]. have [o x_o] : exists o, x o = v. { have vH : v \in H. have/cliques_subset/subsetP := maxcliquesW (maxK j). by apply; move/(_ v): vP; rewrite !inE eqxx => /andP[-> _]. by exists (enum_rank_in vH v); rewrite /x enum_rankK_in. } subst v; rewrite (bigD1 o) //= setIC vP inE eqxx /=. have x_inj : injective x by apply: enum_val_inj. under eq_bigr => z Hz do rewrite vP inE (inj_eq x_inj) (negbTE Hz) (_ : Posz 0 = 0 *+ 0)%R //. by rewrite GRing.sumrMnr mul0rn. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring) mathcomp(ssrint) mathcomp(all_algebra)