proposition: Lemma whites_add_blacks e x : whites (add_blacks x e) = whites e :\ x.
proof: Proof. rewrite whitesE grays_add_blacks /=; apply/setP=> y; rewrite !inE. by case: (_ == _) (_ \in _) (_ \in _) => [] []. Qed.
imports: mathcomp(all_ssreflect) bigmin extra