proposition: Lemma add_blacks_ewf x e : x \in grays e -> wf_env e -> wf_env (add_blacks 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 grays_add_blacks !inE. have [->|] := altP (y =P x); case: colorP => //. by case: colorP x_gray. Qed.
imports: mathcomp(all_ssreflect) bigmin extra