proposition: Lemma limitR_same2 x: CauchyR x -> exists2 y, CauchyQ y & similar_seq x (BR_seq_of_Q y).
proof: Proof. move => cx. pose k n := (BQinv (BQ_of_nat (csucc n))). have Ha: forall n, natp n -> inc (k n) BQps. by move => n nN; apply: QpsS_inv; apply: BQpsS_fromN. pose p x n y := ratp y /\ BRabs (x -r (BR_of_Q y)) <r (BR_of_Q (k n)). pose the_y x n := choose (p x n). have the_yp: forall x n, realp x -> natp n -> p x n (the_y x n). move => z n xr nn; move:(Ha _ nn) => kp;move:(BQ_denseR xr kp) =>[y ya yb]. have Hb:exists y, p z n y by exists y; split. apply:(choose_pr Hb). set y := Lg Nat (fun n => the_y (Vg x n) n). have fgy: fgraph y by rewrite /y; fprops. have dy: domain y = Nat by rewrite /y; aw. move: cx => [[pa pb pc] pd]. have sy: BQ_seq y. split => // t /(range_gP fgy) [n]; rewrite dy => na ->. have zr: realp (Vg x n) by apply:BR_seq_prop. rewrite /y LgV//; exact :(proj1 (the_yp _ _ zr na)). have Hb: forall n m, natp n -> natp m -> n <=c m -> (k m) <=q BQinv (BQ_of_nat (csucc n)). move => n m nN mN h. apply/(BQinv_mon1 (BQpsS_fromN mN) (BQpsS_fromN nN)). by apply/(qle_cN (NS_succ nN) ((NS_succ mN))); apply:cleSS. have cy: CauchyQ y. split => // e ep. move: (BQhalf_pos ep) => e1p; move:(BQhalf_pos e1p) => e2p. move:(pd _ e1p) => [n1 n1N Hc]. move:(BQpsS_fromN_large e2p) => [n2 n2N Hd]. move:(cmax_p1 (CS_nat n1N)(CS_nat n2N)); set N := cmax _ _ ; move => [ka kb]. have NN: natp N by apply:Gmax_E. exists N => // n m nN mN le1 le2. have xnr: realp (Vg x n) by apply: BR_seq_prop. have xmr: realp (Vg x m) by apply: BR_seq_prop. move: (the_yp _ _ xnr nN)(the_yp _ _ xmr mN) =>[ua ub][va vb]. move: (qle_ltT (Hb n2 n n2N nN (cleT kb le1)) Hd) => lt1. move: (qle_ltT (Hb n2 m n2N mN (cleT kb le2)) Hd) => lt2. move /(rlt_cQ (proj31_1 lt1) (proj32_1 lt1)): lt1 => lt3. move /(rlt_cQ (proj31_1 lt2) (proj32_1 lt2)): lt2 => lt4. move:(rlt_ltT ub lt3) => lt5. move:(rlt_ltT vb lt4) => lt6. move: (Hc n m nN mN (cleT ka le1) (cleT ka le2)) => lt7. move: (BRsum_Mltlt (BRsum_Mltlt lt7 lt5) lt6). move:(BQps_sBQ e2p) (BQps_sBQ e1p) => e2q e1q. move: (RS_of_Q (BQps_sBQ e1p)) (RS_of_Q e2q) => qa qb. move: (RS_of_Q ua) (RS_of_Q va) => ua' va'. rewrite (BRabs_diff xnr ua'). move: (RS_diff xnr xmr) (RS_diff ua' xnr)(RS_diff xmr va') => ur vr wr. rewrite - (BRsumA qa qb qb) (BRsum_cQ e2q e2q) (BQdouble_half1 e1q); rewrite (BRsum_cQ e1q e1q) (BQdouble_half1 (BQps_sBQ ep)) => la. move:(rle_triangular ur vr) => lb. move/(BRsum_le2r (proj31 lb) (proj32 lb) (RSa wr)):lb => lc. move:(rle_ltT (rleT (rle_triangular (RSs ur vr) wr) lc) la). rewrite (BRsumC (Vg x n -r Vg x m)) (BRsumA (RS_diff ua' xnr) xnr (RSo xmr)). rewrite (BRsum_diff1 xnr ua') (BRsumA (RS_diff ua' xmr) xmr (RSo va')). rewrite (BRsum_diff1 xmr ua'). rewrite -/(_ -r _ ) (BRdiff_cQ ua va) (BRabs_cQ (QS_diff ua va)). move / (rlt_cQ (QSa (QS_diff ua va)) (BQps_sBQ ep)). rewrite /y !LgV//. have sxy: similar_seq x (BR_seq_of_Q y). move => e ep; move: (BQpsS_fromN_large ep) => [n na nb]. exists n => // m mN mn. move:(qle_ltT (Hb _ _ na mN mn) nb) => nc. move/(rlt_cQ (proj31_1 nc) (proj32_1 nc)): nc => nd. have zr: realp (Vg x m) by apply:BR_seq_prop. move:(rlt_ltT (proj2 (the_yp _ _ zr mN)) nd). rewrite /BR_seq_of_Q /y !LgV//. by exists y. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)