proposition: Lemma min_imperfect_stabsets_cliques H (a := α(H)) (w := ω(H)) (k := (a*w).+1) : min_imperfect H -> exists S K : 'I_k -> {set G}, [/\ (forall i, S i \in stabsets H), (forall i, K i \in maxcliques H), (forall x, x \in H -> \sum_i (x \in S i) = a), (forall i, [disjoint K i & S i]) & (forall i j : 'I_k , i != j -> #|K i :&: S j| = 1)].
proof: Proof. move => minH. move: (leqnn a); rewrite {2}/a; case: alphaP => [S0 maxstabS _]. have colSv (v : { v | v \in S0}) : { P | coloring P (H :\ tag v) & #|P| == w }. { case: v => v v_S0; apply: sig2W => /=. have vH: v \in H by apply: (subsetP (maxstabsetS maxstabS)). have : χ(H :\ v) = w. rewrite -perfect_eq ?min_imperfectD //. by rewrite inE stable1 sub1set andbT. apply: proper_min_imperfect minH; exact:properD1. by case: chiP => P colP _ /eqP ?; exists P. } pose col v := if insub v is Some v' then s2val (colSv v') else set0. pose s := S0 :: flatten [seq enum (col v) | v <- enum S0]. have size_s : size s == k. { rewrite /s/k /= eqSS size_flatten /shape sumnE !big_map big_enum /=. under eq_bigr => x x_S0 do rewrite /col insubT -cardE /= (eqP (s2valP' (colSv (Sub x x_S0)))). by rewrite sum_nat_const (card_maxstabset maxstabS). } pose S (i : 'I_k) := tnth (Tuple size_s) i; exists S. have stabS i : S i \in stabsets H. { have := mem_tnth i (Tuple size_s); rewrite /S/=; set Si := tnth _ _. rewrite !inE => /predU1P [->|]. by move/maxstabsetW : maxstabS; rewrite inE => /andP[-> ->]. move=> /flattenP => -[/= ?] /mapP [v v_S0 ->]; rewrite !mem_enum in v_S0 *. rewrite /col insubT; case: (colSv _) => /= P /andP[partP stabP] _ SiP. rewrite (forall_inP stabP) // andbT. exact: subset_trans (partitionS partP SiP) (subsetDl _ _). } have cutS x : x \in H -> \sum_(i < k) (x \in S i) = a. { move => xH. rewrite sum_cond1 /= sum1dep_card /S (tuple_index_count _ (fun S' => x \in S')). rewrite /s /= count_flatten !sumnE !big_map big_enum /= /a. have count_S v : v \in S0 -> count (fun S' => x \in S') (enum (col v)) = (v != x). { move=> v_S0. rewrite /col insubT; case: (colSv _) => /= P /andP[partP _] _. rewrite count_enum_cards trivIset_mem; last exact/partition_trivIset/partP. by rewrite (cover_partition partP) !inE xH 1?eq_sym andbT. } under eq_bigr => v vS0 do rewrite count_S //. rewrite -[RHS](card_maxstabset maxstabS) -sum1_card sum_cond1. have [x_S0|xNS0] := boolP (x \in S0). - by rewrite [RHS](bigD1 x) //=. - rewrite add0n big_mkcondr; apply: eq_bigr => v. case: (eqVneq x v) => [<-|//]. by rewrite (negbTE xNS0). } have cl (i : 'I_k) : { C | C \in maxcliques H & [disjoint C & S i] }. exact/sig2W/min_imperfect_maxclique. pose K (i : 'I_k) := s2val (cl i). have maxK (i : 'I_k) : K i \in maxcliques H by exact: (s2valP (cl i)). have disjK (i : 'I_k) : [disjoint K i & S i] by exact: (s2valP' (cl i)). exists K; split => //. have le_KiSj i j : #|K i :&: S j| <= 1. { apply: cliqueIstable; first exact:maxclique_clique. by case/stabsetsP : (stabS j). } have KiSi0 i : #|K i :&: S i| = 0 by apply/eqP; rewrite cards_eq0 setI_eq0. have sum_j i : \sum_(j | i != j) #|K i :&: S j| >= a * w. { have <- : #|K i| = w by apply/card_maxclique/(s2valP (cl i)). rewrite -sum1_card sum_nat_mulnr. under eq_bigr => x x_Ki; first rewrite muln1 -(cutS x); first over. move: x x_Ki; apply/subsetP. by move: (maxK i); rewrite !inE -andbA => /and3P[]. rewrite exchange_big/=. under eq_bigr => j do rewrite sum_cardI. by rewrite [X in _ <= X]big_rmcond // => j /negPn/eqP<-. } move => i j iDj; apply: contraTeq (sum_j i). rewrite eqn_leq negb_and le_KiSj -leqNgt leqn0 /= -ltnNge => /eqP KiSj0. rewrite (bigD1 j) //= KiSj0 add0n. apply: (@leq_ltn_trans (\sum_(i0 < k | (i != i0) && (i0 != j)) 1)). exact: leq_sum => o _. rewrite sum1_card /= -ltnS -/k -[X in _ < X]card_ord. set p := fun _ => _; rewrite -(cardC p) -addn1 addSn -addnS leq_add2l. by apply/card_gt1P; exists i,j; rewrite !inE iDj !unfold_in !eqxx /= andbF. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring) mathcomp(ssrint) mathcomp(all_algebra)