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