proposition: Lemma nth_elt_inK K n: natp n -> sub K Nat -> n <c cardinal K -> inc (nth_elt K n) K.
proof: Proof. by move => pa pb pc; move:(nth_set7 pa pb pc) => [/setC_P []]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)