proposition: Lemma sub_nat_finite K n: natp n -> sub K n -> natp (cardinal K).
proof: Proof. move => nN /sub_smaller; rewrite (card_nat nN) => h; apply:(NS_le_nat h nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)