proposition: Lemma new_stackE e1 e2 : subenv e1 e2 -> new_stack e1 e2 = [set x | sn e1 <= num e2 x < sn e2].
proof: Proof. move=> sube12; apply/setP=> x; rewrite !inE. have [x_e2|] := ltnP (num e2 x) (sn e2); rewrite ?andbT ?andbF//. have [e1_after|e1_before] /= := leqP (sn e1) (num e1 x). by rewrite leqNgt -sub_num_lt// -leqNgt. by rewrite leqNgt -sub_num_lt// e1_before. Qed.
imports: mathcomp(all_ssreflect) extra_nocolors