proposition: Lemma BR_limit_of_rat x: realp x -> exists2 s, CauchyQ s & limitR (BR_seq_of_Q s) x.
proof: Proof. move => xr. have[C ca [[cb cc cd ce cf] cg]]: exists2 C, BQpairR C = x & BQpair C. case: (BR_rational_dichot xr) => rx. move: (BR_of_Q_prop2 rx) => [y ry yv]. move:(BQpair_rational2 ry) => [c [ca cb _]]; exists c => //; ue. move:(BQpair_irrational3 rx) => [c [ca cb _]]; exists c => //; ue. set s := Lg Nat (fun n => Q (Vg C n)). have fgs: fgraph s by rewrite /s; fprops. have ds: domain s = Nat by rewrite /s; aw. have Ha: forall n, natp n -> ratp (Q (Vg C n)). by move => n /cd /setX_P[_ _]. have Hb: forall n, inc n Nat -> ratp (Vg s n). by rewrite /s => n nn; rewrite LgV//; apply: Ha. have ss: BQ_seq s. by split => // t /(range_gP fgs); rewrite ds; move => [y ua ->]; apply: Hb. have Cdec: forall n m, natp n -> natp m -> n <=c m -> (Q (Vg C m)) <=q (Q (Vg C n)). move => n m nn mn lemn. rewrite - (cdiff_pr lemn); move: (NS_diff n mn). move: (m -c n); apply: Nat_induction. rewrite (csum0r (CS_nat nn)); apply:qleR; fprops. move => k kN Hrec; rewrite (csum_nS _ kN). exact:(qleT (proj1 (cf _ (NS_sum nn kN))) Hrec). have Hc: forall n, natp n -> inc (Q (Vg C n)) x. move => n nn; rewrite - ca; apply/Zo_P; split; first by apply: Ha. exists (csucc n);fprops. have cs: CauchyQ s. split => // e ep; move:(BRi_lowbound xr ep) => [y yx Hy]. move: yx; rewrite - ca => /Zo_P[yq[n na nb]]; exists n => //. move => n1 n2 n1n n2n nc nd. wlog n1n2: n1 n2 n1n n2n nc nd / n1 <=c n2. move => H; case: (NleT_ee n1n n2n) => ele; first by apply:H. rewrite BQabs_diff; fprops. have hc: inc (Q (Vg C n1) -q Q (Vg C n2)) BQp. move: (Cdec _ _ n1n n2n n1n2) => sa. by move /(qle_diffP1 (proj31 sa) (proj32 sa)) : sa => / qle0xP. rewrite /s ! LgV// (BQabs_pos hc). move: (Hy _ (Hc _ n2n)) => /(BQdiff_lt1P yq (BQps_sBQ ep) (Ha _ n2n)) => sa. move: (qle_ltT (Cdec _ _ na n1n nc) nb) => sb. move/(BQsum_lt2r (proj31_1 sb)(proj32_1 sb) (QSo (Ha _ n2n))): sb. move => sc; BQo_tac. exists s => // e ep; move:(BRi_lowbound xr ep) => [y yx Hy]. move: yx; rewrite - {1} ca => /Zo_P[yq[n na nb]]; exists n => //. move: (BQps_sBQ ep) => eq. have ha: BR_of_Q (y -q e) <=r x. by apply:(BR_le_aux3 xr (QS_diff yq eq)) => /Hy [_]. move => m mN nm. move: (qle_ltT (Cdec _ _ na mN nm) nb) => sb. move/(BQsum_lt2r (proj31_1 sb)(proj32_1 sb) (QSo eq)): sb => sc. move /(rlt_cQ (proj31_1 sc)(proj32_1 sc)): sc => sd. rewrite /BR_seq_of_Q /s !LgV//. have sa: (inc (BR_of_Q (Q (Vg C m)) -r x) BRp). move: (proj1 (BR_le_aux2 xr (Hc _ mN))) => sa. by apply/ rle0xP; apply/ (rle_diffP1 (proj31 sa) (proj32 sa)). rewrite /BRabs (Y_true sa). apply / (BRdiff_lt1P (RS_of_Q (Ha _ mN)) xr (RS_of_Q (BQps_sBQ ep))). rewrite (BRdiff_cQ (Ha _ mN) (BQps_sBQ ep)); BRo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)