proposition: Lemma Exercise5_9j4 q p: natp q -> \0c <c q -> Zo p (Ex59_intervalp q) = Ex59_splitA' q p.
proof: Proof. move => qN qp. set_extens t. move => tv; move:(tv)=> /Zo_P[ti it]; apply /funI_P. rewrite(Exercise5_9j2 qN qp it). by exists (Ex59_int_lb q t); [ apply/funI_P; ex_tac | ]. move/funI_P =>[z /funI_P [u uz ->] ->]. by rewrite -(Exercise5_9j2 qN qp (Zo_hi uz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)