proposition: Lemma maxstabset_coloring (G : sgraph) (P : {set {set G}}) (D : {set G}) : partition P D -> {in P, forall S, S \in maxstabsets D} -> χ(D) = #|P|.
proof: Proof. move=> partP maxP; have [D0|[x xD]] := set_0Vmem D. by subst D; apply/esym/eqP; rewrite chi0 cards_eq0 -partition_set0. have colP : coloring P D. by apply/coloring_stabsetP; split => // B /maxP/maxstabsetW. apply/eqP; rewrite eqn_leq (color_bound colP) /=. have [P' /coloring_stabsetP[partP' stabP'] _] := chiP. have [trivP trivP'] : trivIset P /\ trivIset P'. by case/and3P : partP; case/and3P : partP'. apply: contraTT (leqnn #|D|); rewrite -!ltnNge => lt_P'_P. rewrite -{1}(cover_partition partP') -(cover_partition partP). rewrite -(eqP trivP) -(eqP trivP'). under [X in _ < X]eq_bigr => B BP do rewrite (card_maxstabset (maxP _ BP)). apply: (@leq_ltn_trans (#|P'| * α(D))). by rewrite -sum_nat_const; apply: leq_sum => B /stabP'; apply: stabset_bound. rewrite sum_nat_const ltn_mul2r lt0n alpha_eq0 lt_P'_P andbT. by apply/set0Pn; exists x. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)