proposition: Lemma nth_elt_ax K: sub K Nat -> natp (cardinal K) -> lf_axiom (nth_elt K) (cardinal K) K.
proof: Proof. move => KN kN n /(NltP kN) nk. apply: (nth_elt_inK (NS_lt_nat nk kN) KN nk). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)