proposition: Lemma num_lt_V x : (num e x < infty) = (num e x < sn e).
proof: Proof. apply/idP/idP => [/num_lt_V_is_stack//|]; first exact. by move=> /leq_trans; apply; rewrite max_card. Qed.
imports: mathcomp(all_ssreflect) extra_nocolors