proposition: Lemma coloringD1 P S H : coloring P H -> S \in P -> coloring (P :\ S) (H :\: S).
proof: Proof. move=> /andP[partP stabP] SP; apply/andP; split; first exact: partitionD1. by apply/forall_inP => A /setD1P[_ /(forall_inP stabP)]. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)