proposition: Lemma chi_clique C : clique C -> χ(C) = #|C|.
proof: Proof. move=> clique_C; apply/eqP; rewrite eqn_leq leq_chi /=. have [P /andP[partP /forall_inP /= stabP] opt_P] := chiP. suff S A : A \in P -> #|A| = 1. { rewrite (card_partition partP); under eq_bigr => A ? do rewrite S //. by rewrite sum_nat_const muln1. } move=> AP; apply/eqP; rewrite eqn_leq card_gt0 (partition_neq0 partP) //. rewrite andbT -(@setIidPl _ A C _) ?(partitionS partP) // setIC. exact : cliqueIstable (stabP _ _). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)