proposition: Lemma coloring_stabsetP P D : reflect (partition P D /\ {in P, forall B, B \in stabsets D}) (coloring P D).
proof: Proof. apply: (iffP andP) => -[partP stabP]; split => //; [|apply/forall_inP] => B BP. by rewrite inE (partitionS partP) ?(forall_inP stabP). by move/stabP : BP; rewrite !inE => /andP[_ ->]. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)