proposition: Lemma num_stackP e x : wf_color e -> wf_num e -> (x \in stack e) = (0 < num e x < sn e).
proof: Proof. move=> e_cwf e_nwf; symmetry; rewrite lt0n wf_num0//; case: stackP => //=. by move=> x_stack; rewrite wf_num_lt // wf_num_infty//; case: stackP x_stack. by rewrite -wf_num_infty => // /eqP->; rewrite ltnNge sn_small. Qed.
imports: mathcomp(all_ssreflect) bigmin extra