proposition: Lemma subenv_gray_le e1 e2 x y : subenv (add_stack x e1) e2 -> wf_color e2 -> wf_num e2 -> y \in gray e2 -> num e2 y <= num e2 x.
proof: Proof. move=> subxe12 e2_cwf e2_nwf y_gray. case: (@subenv_stackP (add_stack x e1) e2) => // s s_def sb. rewrite wf_num_stack //; last 2 first. - by case: color4P y_gray. - by rewrite s_def mem_cat /= mem_head orbT. rewrite s_def !index_cat. rewrite !ifN /=; first by rewrite leq_add2l eqxx; case: ifPn => //=. by apply: contraTN y_gray => /(subsetP sb); case: color4P. have := wf_uniq e2_cwf; rewrite s_def => /(@uniq_catRL _ x). by rewrite mem_cat mem_head orbT -s_def wf_uniq// => <-. Qed.
imports: mathcomp(all_ssreflect) bigmin extra