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