proposition: Lemma omega_leq_chi A : ω(A) <= χ(A).
proof: Proof. case: omegaP => C; rewrite !inE -andbA => /and3P[subCA /cliqueP clique_C _]. by apply: leq_trans (sub_chi subCA); rewrite chi_clique. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)