proposition: Lemma leq_num_infty e x : wf_num e -> (num e x) <= infty.
proof: Proof. move=> [_ _ /(_ x)]; case: eqP => [->|_ nLs snE _] //. by rewrite -ltnS (leq_trans (nLs _)) // snE ltnS (leq_trans (max_card _)). Qed.
imports: mathcomp(all_ssreflect) bigmin extra