proposition: Lemma new_white e1 e2 : wf_color e2 -> subenv e1 e2 -> white e1 :\: white e2 = black e2 :\: black e1.
proof: Proof. move=> e2_wf e12; rewrite whiteE -(subenv_gray e12) setDE setCK setIC -setDE. rewrite setDUl setDE setCU setIA setICr set0I set0U. rewrite setDUr (setIidPr _) // [_ :\: gray _](setDidPl _) ?subsetDl //. by apply/pred0P => y /=; case: color4P. Qed.
imports: mathcomp(all_ssreflect) bigmin extra