proposition: Lemma nth_elt_prop7 K n s: natp n -> inc K (\Po n) -> inc s (permutations (cardinal K)) -> nonempty K -> inc (nth_elt K (Vf s \0c)) K.
proof: Proof. move => nN /setP_P Kn /permutationsP [[[fs _] _] ss ts] ke. have sKN: sub K Nat by move => t /Kn/(NltP nN) => h;apply(NS_lt_nat h nN). move:(sub_smaller Kn); rewrite (card_nat nN) => ckn. have ckN:=(NS_le_nat ckn nN). have cknz:= (card_nonempty1 ke). have zi: inc \0c (cardinal K). apply /(NltP ckN); split; [ apply: (cle0n ckN) | fprops]. have l1: (Vf s \0c) <c cardinal K by apply/(NltP ckN); Wtac; rewrite ss. by move:(nth_set7 (NS_lt_nat l1 ckN) sKN l1) => [/setC_P []]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)