proposition: Lemma stack_neq_infty e x : wf_color e -> wf_num e -> x \in stack e -> (num e) x != infty.
proof: Proof. by move=> e_cwf e_nwf x_stack; rewrite wf_num_infty// stack_sccsF. Qed.
imports: mathcomp(all_ssreflect) bigmin extra