proposition: Lemma Exercise5_9l3 n q p k (E:= Nint (q *c n)): natp n -> natp q -> \0c <c q -> inc p (Ex59_k_interval E q k) -> Ex59_Cprop n q (Ex59_splitA q p) k (Ex59_splitB q p).
proof: Proof. move => nN qN qp pi. have ce:cardinal E = q *c n by apply:card_Nint; fprops. have cp:=(Exercise5_9j6 nN qN qp ce pi). split => //. apply:Exercise5_9l2 => //; apply/Zo_S: pi. rewrite /Ex59_splitB - (Exercise5_9j4 _ qN qp). by move => x /setC_P [xp /Zo_P xx] xe; case:xx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)