proposition: Lemma nth_set4 K S (S':= nth_more K S) (x:= intersection (K -s S)): sub K Nat -> segment_nat K S -> S <> K -> [/\ segment_nat K S', inc x (S' -s S) & cardinal S' = csucc (cardinal S)].
proof: Proof. move => KN [sa sb sc]. have sd:=(setC_ne (conj sa sc)). have se:=(sub_trans (@sub_setC K S) KN). move:(inf_Nat se sd); rewrite -/x; move => [/setC_P [xK xS] xm]. split; first split. + by move => t /setU1_P; case; [move /sa | move => ->]. + move => i j /setU1_P iv /setC_P [jK /setU1_P jv]. have [js /nesym ji]: ~(inc j S) /\ j <> intersection (K -s S). by split;dneg h; fprops. have aux: inc j (K -s S) by apply/setC_P. case iv; first by move => iS; apply: sb => //. by move ->; split => //; apply: xm. + by apply/setC_P; split; [ apply:setU1_1 | ]. + by rewrite csucc_pr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)