proposition: Lemma white_add_black e x : white (add_black x e) = white e :\ x.
proof: Proof. rewrite whiteE gray_add_black /=; apply/setP=> y; rewrite !inE. by case: (_ == _) (_ \in _) (_ \in _) => [] []. Qed.
imports: mathcomp(all_ssreflect) bigmin extra