proposition: Lemma sub_chi A B : A \subset B -> χ(A) <= χ(B).
proof: Proof. move=> subAB; case: (chiP B) => P col_P opt_P. have col_S := sub_coloring col_P subAB. apply: leq_trans (color_bound col_S) (card_sub_partition _ subAB). by case/andP : col_P. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)