proposition: Lemma preim_coloring (P : {set {set G}}) (D : {set F}) : coloring P (i @: D) -> coloring [set i @^-1: (B : {set G}) | B in P] D.
proof: Proof. move => colP; rewrite coloring_isubgraph -imset_comp /comp /=. have coB B : B \in P -> B \subset codom i. { case/andP: colP => partP _; move/(partitionS partP) => sub. apply: subset_trans sub _. exact: imset_codom. } under [X in coloring X _]eq_in_imset => B BP. rewrite (can_preimset i) ?coB //; over. by rewrite imset_id. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)