proposition: Lemma coloring_isubgraph (P : {set {set F}}) (D : {set F}) : coloring P D = @coloring G [set i @: (S : {set F}) | S in P] (i @: D).
proof: Proof. rewrite /coloring -imset_partition; last exact: isubgraph_inj. by rewrite forall_imset; under [in RHS]eq_forallb => S do rewrite -stable_isubgraph. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)