proposition: Lemma add_stack_gwf e w : access_to e [set w] -> wf_color e -> wf_num e -> w \in white e -> wf_graph e -> wf_graph (add_stack w e).
proof: Proof. move=> gray_to e_cwf e_nwf w_white [gs sg]; split. move => x y. rewrite !ffunE !inE /=. have [-> _|neq_xw /= x_stack] := altP eqP; have [-> _|neq_yw /= y_stack]// := altP eqP. - by rewrite leqNgt wf_num_lt// stack_neq_infty. - case/sg: x_stack => z [/gray_to zCs _ xCz] _. apply: connect_trans (zCs _ _) => //. by rewrite !inE. - exact: gs. move=> y; rewrite inE => /predU1P [->|]. by exists w; rewrite ?gray_add_stack ?inE ?eqxx. move=> y_stack; have /sg [x [x_gray le_xy y_to_x]] := y_stack. exists x; split=> //; first by rewrite gray_add_stack // inE x_gray orbT. rewrite /= !ffunE/= !ifN//; apply: contraTneq w_white => <-; by case: color4P y_stack x_gray. Qed.
imports: mathcomp(all_ssreflect) bigmin extra