proposition: Lemma color_bound P A : coloring P A -> χ(A) <= #|P|.
proof: Proof. by move => col_P; case: chiP => P' _ /(_ _ col_P). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)