proposition: Lemma sub_coloring P D A : coloring P D -> A \subset D -> coloring (sub_partition P A) A.
proof: Proof. case/andP => partP /forall_inP/= stabP subAD; apply/andP;split. exact: sub_partitionP. have/subsetP sub := sub_partition_sub partP subAD. apply/forall_inP => S {}/sub /imsetP [B BP ->]. by apply: sub_stable (stabP _ BP); apply: subsetIl. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)