proposition: Lemma add_black_nwf x e : x \in gray e -> wf_color e -> wf_num e -> wf_num (add_black x e).
proof: Proof. move=> x_g wf_c wf_e. have [nEw nEc nLs snE pE] := wf_e. split => //= [y|]. by rewrite white_add_black !inE nEw; case: eqP => // ->; case: color4P x_g. by rewrite gray_add_black setUA /= [_ :|: [set x]]setUC setD1K. Qed.
imports: mathcomp(all_ssreflect) bigmin extra