proposition: Lemma nth_set5 K n (S:= nth_elts K n): natp n -> sub K Nat -> n <=c cardinal K -> (segment_nat K S /\ cardinal S = n).
proof: Proof. rewrite /S => nN kN;move: n {S} nN; apply: Nat_induction. by rewrite nth_elts0 cardinal_set0; split=> //; split=> [ i | i j ] /in_set0. move => n nN Hrec snk. rewrite /nth_elts (induction_terms _ _ nN) -/(nth_elts K n). move:(Hrec (cleT (cleS nN) snk)) => [sa sb]. case (equal_or_not (nth_elts K n) K) => nsK. by move: (proj2 (clt_leT (cltS nN) snk)); rewrite - nsK sb. by move: (nth_set4 kN sa nsK); rewrite sb; move => [ua _ ub]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)