proposition: Lemma BQ_denseR2 x: realp x -> (exists2 y, ratp y & x <r (BR_of_Q y)) /\ (exists2 y, ratp y & (BR_of_Q y) <r x).
proof: Proof. move => xr; move:(BQ_denseR xr QpsS1) =>[y yq]. move /(BRabs_prop4 xr (RS_of_Q yq) RS1) =>[]. rewrite (BRdiff_cQ yq QS1) (BRsum_cQ yq QS1) => sa sb. split; first by exists (y +q \1q) => //;exact:(QSs yq QS1). exists (y -q \1q) => //;exact:(QS_diff yq QS1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)