proposition: Lemma Exercise5_9j3 q p j: natp q -> \0c <c q -> inc j (Ex59_splitA q p) -> (natp j /\ inc (Ex59_int q j) p).
proof: Proof. move => qN qp /funI_P [z /Zo_P [za zb] zc]. by move:(Exercise5_9j1 qN qp zb); rewrite - zc; move => [<- jN]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)