proposition: Lemma add_stack_gwf e w : access_to e [set w] -> wf_env e -> w \in whites e -> wf_graph e -> wf_graph (add_stack w e).
proof: Proof. move=> grays_to e_wf w_white [gs sg]; split. - rewrite grays_add_stack //= => x y; rewrite rank_cons !inE. move=> /orP[/eqP->|/andP[xNb xs]] /orP[/eqP->|/=ys]; rewrite ?rank_cons ?eqxx ?(@whites_stackF w) ?xs ?ys ?(andbF, andbT) //=. + by rewrite leqNgt rank_small ?wf_stack_uniq // ys. + by move=> _; rewrite grays_to ?inE //= xNb. + by apply: gs; rewrite ?inE ?xNb. - move=> y; rewrite inE => /predU1P [->|]. exists w; rewrite ?grays_add_stack ?inE ?eqxx //. by rewrite whites_blacksF ?whites_stackF. move=> y_stack; have /sg [x [x_gray le_xy y_to_x]] := y_stack. exists x; split=> //. by rewrite grays_add_stack // inE x_gray orbT. rewrite stack_add_stack !rank_cons [x == w]negbTE /= 1?[y == w]negbTE //=. by apply: contraTneq y_stack => ->; rewrite whites_stackF. by apply: contraTneq x_gray => ->; rewrite whites_graysF. Qed.
imports: mathcomp(all_ssreflect) extra