proposition: Lemma add_black_cwf x e : x \in gray e -> wf_color e -> wf_color (add_black x e).
proof: Proof. move=> x_gray e_wf; split => //=; last 2 first. - by rewrite subsetU // wf_sccs // orbT. - exact: wf_uniq. move=> y; rewrite gray_add_black !inE. have [->|] := altP (y =P x); case: color4P => //. by case: color4P x_gray. Qed.
imports: mathcomp(all_ssreflect) bigmin extra