proposition: Lemma add_stack_cwf x e : x \in white e -> wf_color e -> wf_color (add_stack x e).
proof: Proof. move=> x_white e_wf; split=> /=; do ? by [exact: wf_sccs|rewrite white_stackF ?wf_uniq]. move=> y; rewrite gray_add_stack // !inE. by case: (_ == _) color4P => [] []. Qed.
imports: mathcomp(all_ssreflect) bigmin extra