proposition: Lemma coloringU1 P S H : stable S -> S != set0 -> coloring P H -> [disjoint S & H] -> coloring (S |: P) (S :|: H).
proof: Proof. move=> stS SD0 /andP[partP stabP] disHS; apply/andP; split; first exact: partitionU1. by apply/forall_inP => A /setU1P[-> //|/(forall_inP stabP)]. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)