proposition: Lemma nth_set7 K n (S:= (nth_elts K n)) (x:= nth_elt K n) : natp n -> sub K Nat -> n <c cardinal K -> [/\ inc x (K -s S), inc x (nth_elts K (csucc n)), forall y, inc y (K -s S) -> x <=c y & forall y, inc y S -> y <c x].
proof: Proof. move => nN KN h1. have [[SK sw] cs1]:= (nth_set5 nN KN (proj1 h1)). have pa: sub (K -s S) Nat by move => t/setC_P [/ KN h _]. case: (emptyset_dichot (K -s S)) => nek. by case: (proj2 h1); rewrite - cs1 {2} (extensionality (empty_setC nek) SK). have h2: csucc n <=c cardinal K by apply /(cleSltP nN). move: (inf_Nat pa nek). set I := intersection (K -s S); move => [sa sb]. have /setCId_Pl di: disjoint (singleton I) S. by apply: disjoint_pr => u /set1_P -> eis; case/setC_P: sa => _. move: (erefl x); rewrite {1} /x /nth_elt /nth_elts (induction_terms _ _ nN). rewrite -/(nth_elts K n) /nth_more -/S -/I setCU2_l setC_v set0_U2 di setU_1. by move => <-; split; fprops; move => y ys; apply: sw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)