proposition: Lemma Exercise5_9j2 q x (j := Ex59_int_lb q x): natp q -> \0c <c q -> Ex59_intervalp q x -> x = Ex59_int q j.
proof: Proof. move => ha hb hc; exact: (proj1 (Exercise5_9j1 ha hb hc)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)