proposition: Lemma nth_elt_prop8 K n a: natp n -> inc K (\Po n) -> inc a K -> exists2 f, inc f (permutations (cardinal K)) & a = nth_elt K (Vf f \0c).
proof: Proof. move => nN Ks1 aK. have neK: nonempty K by ex_tac. move/setP_P: (Ks1) => ka. have sKN:= (sub_trans ka (NS_inc_nat nN)). move:(sub_smaller ka); rewrite (card_nat nN) => ckn. have cknz:= (card_nonempty1 neK). have ckN:=(NS_le_nat ckn nN). move:(cpred_pr ckN cknz); set k:= cpred _; move => [kN kv]. have fsk: finite_set K by apply/NatP. move:(nth_elt_surj sKN ckN aK) => [i il1 ->]. move: (permutation_exists1 ckN il1) => [f fp <-]; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)