proposition: Lemma leq_chi A : χ(A) <= #|A|.
proof: Proof. case: chiP => C col_C /(_ _ (@trivial_coloringP _ A)). rewrite /trivial_coloring card_imset //. exact: set1_inj. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)