proposition: Lemma add_stack_pre e w : access_to e [set w] -> wf_color e -> w \in white e -> wf_graph e -> access_to (add_stack w e) [set x in successors w].
proof: Proof. move=> gray_to e_wf w_white e_gwf. move=> x y; rewrite gray_add_stack // !inE => /predU1P [->|]. by move=> y_succ_w; rewrite connect1. move=> /gray_to x_to_y y_succ_w. by rewrite (connect_trans _ (connect1 y_succ_w)) // x_to_y ?inE. Qed.
imports: mathcomp(all_ssreflect) bigmin extra