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