proposition: Lemma BR_of_Q_prop1 x: ratp x -> rationalp (BR_of_Q x).
proof: Proof. move => xq; set E := (BR_of_Q x). have pa: inc x (BQ -s E) by apply /setC_P; split => // /Zo_P [_][]. split; last first. move => [_ h]; move: (h x pa) => [y /setC_P [ya yb] yc]. by case: yb; apply: Zo_i. have H: forall y, x <q y -> inc y E. move => y yy; apply:Zo_i=> //;exact:(proj32_1 yy). split. + by apply: Zo_S. + by exists (x +q \1q); apply:H; apply: qlt_succ. + move => h; move: pa; rewrite h setC_v; case; case. + move => y z /Zo_P [pb pc] pd; apply: H; BQo_tac. + move => y /Zo_P[ya /BQmiddle_comp [yb yc]]. by exists (BQmiddle x y) => //; apply:H. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)