proposition: Lemma chiP A : chi_spec A χ(A).
proof: Proof. rewrite /chi_mem; case: arg_minnP; first exact: trivial_coloringP. by move=> P; rewrite setE => ? ?; apply: ChiSpec. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)