proposition: Lemma BQ_denseR x e: realp x -> inc e BQps -> exists2 y, ratp y & BRabs (x -r (BR_of_Q y)) <r (BR_of_Q e).
proof: Proof. move => xr ep. case: (BR_rational_dichot xr) => rx. move:(BR_of_Q_prop2 rx) => [y yq yv]; exists y => //; rewrite -yv. by rewrite (BRdiff_xx xr) BRabs_0; apply / rlt0xP; apply: RpsS_of_Q. move: (proj2 rx) => sa. move:(BRi_lowbound xr ep) => [y yx Hy]. move: (BRi_sQ xr yx) (BQps_sBQ ep) => yq eq. move:(BR_le_aux2 xr yx) =>/ (rlt_diffP1 xr (RS_of_Q yq)) / rlt0xP => h. exists y => //. have ->: BRabs (x -r BR_of_Q y) = BR_of_Q y -r x. by rewrite (BRabs_diff xr (RS_of_Q yq)) /BRabs (Y_true (BRps_sBRp h)). apply /(BRdiff_lt1P (RS_of_Q yq) xr (RS_of_Q eq)). rewrite (BRdiff_cQ yq eq); split. by apply: (BR_le_aux3 xr (QS_diff yq eq)) => /Hy [_]. move => e2. by move:(proj2 (BR_of_Q_prop1 (QS_diff yq eq))); rewrite e2; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)