proposition: Lemma nth_set6 K (n:= cardinal K): natp n -> sub K Nat -> (nth_elts K n) = K.
proof: Proof. move => nN kN. move: (nth_set5 nN kN (cleR (CS_nat nN))) => [[sa _] sb]. have fsk: finite_set K by apply /NatP. exact: (cardinal_setC5 fsk sa sb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)