proposition: Lemma Exercise5_9l2 n q p (E:= Nint (q *c n)): natp n -> natp q -> \0c <c q -> inc p (partition_nq E q) -> inc (Ex59_splitB q p) (partition_nq (Ex59_compl n q (Ex59_splitA q p)) q).
proof: Proof. move => nN qN qp pp. have ha:=(Exercise5_9l1 nN qN qp pp). move/Zo_P: pp => [/partitionsP [[qa qb] qc] qd]. apply/Zo_P; split; last by move => x /setC_P [/qd]. apply/partitionsP; split;last by move => x /setC_P [/qc]. by split =>// a b /setC_P [ ap _] /setC_P [ bp _]; apply: qb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)