proposition: Lemma Exercise5_9j1 q x (j := Ex59_int_lb q x): natp q -> \0c <c q -> Ex59_intervalp q x -> x = Ex59_int q j /\ natp j.
proof: Proof. move => qN qp h; apply: (select_pr h). move => a b /= aN av bN bv. rewrite av in bv; exact:( Nintcc_exten_spec qN aN bv). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)