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