proposition: Lemma nth_elt_surj K a: sub K Nat -> natp (cardinal K) -> inc a K -> exists2 n, n <c (cardinal K) & a = (nth_elt K n).
proof: Proof. move => ha hb aK; move:(nth_elt_bf ha hb) => [[_ [ff fs]] _]. have ax:= (nth_elt_ax ha hb). move:fs; aw => fs; move:(fs _ aK) => [x xa]; rewrite LfV// => ->. by exists x => //; apply/(NltP hb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)