proposition: Lemma num_lt_card x (A : pred V) : seen e \subset A -> (num e x < #|A|) = (num e x < sn e).
proof: Proof. move=> subeA; apply/idP/idP => /leq_trans. by rewrite -num_lt_V; apply; rewrite max_card. by apply; rewrite subset_leq_card. Qed.
imports: mathcomp(all_ssreflect) bigmin extra