proposition: Lemma Exercise5_9j6 E n q p k: natp n -> natp q -> \0c <c q -> cardinal E = q *c n -> inc p (Ex59_k_interval E q k) -> cardinal (Ex59_splitB q p) = n -c k.
proof: Proof. move => nN qN qp cE px. move:(proj2 (Exercise5_9j5 nN qN qp cE px)) => ck. have ha: sub (Ex59_splitA' q p) p. by rewrite - (Exercise5_9j4 _ qN qp); apply:Zo_S. move:px => /Zo_S pp. have cp:=(partition_nq_pr2 (CS_nat nN) qN (nesym (proj2 qp)) cE pp). have fsp: finite_set p by apply/NatP; rewrite cp. by rewrite /Ex59_splitB (cardinal_setC4 ha fsp) ck cp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)