proposition: Lemma BR_complete1 s: CauchyQ s -> exists2 x, realp x & limitR (BR_seq_of_Q s) x.
proof: Proof. move => cs. have [B Bq Bp]:= (BR_Cauchy_bounded cs). move:cs => [sa sd]. pose Ap t := exists2 n, natp n & forall k, natp k -> n <=c k -> (Vg s k) <=q t. set A := Zo BQ Ap. have neA: nonempty A. exists B; apply/Zo_P; split => //; exists \0c; [ fprops | move => k kN _]. by move: (Bp _ kN) => /(BQabs_prop1 (BQ_seq_prop sa kN) Bq) [_]. have Anq: A <> BQ. have ha:= (QSo (QSs Bq QS1)). case: (inc_or_not (BQopp (B +q \1q)) A); last by move => hb h; case: hb; ue. move => /Zo_P [_ [n nN np]]. have hc: BQopp (B +q \1q) <q BQopp B by apply/ qlt_opp; apply:(qlt_succ Bq). move/(BQabs_prop1 (BQ_seq_prop sa nN) Bq):(Bp _ nN) => [hb _]. move:(qle_ltT (np _ nN (cleR (CS_nat nN))) hc) => hd; BQo_tac. have As1: forall x y, inc x A -> x <=q y -> inc y A. move => x y /Zo_P [xq [n na nb]] xy; apply /Zo_P; split. apply:(proj32 xy). exists n => // k ka kb; move: (nb _ ka kb) => ha; BQo_tac. have As: forall x y, inc x A -> x <q y -> inc y A. move => x y xa [xy _]; apply: (As1 _ _ xa xy). case:(p_or_not_p (exists2 y, inc y A & forall t, inc t A -> y <=q t)). move =>[y / Zo_P[ya yb] yc] ;move:(RS_of_Q ya) => yr. exists (BR_of_Q y) => // e eq; ex_middle bad. have hep:=(BQhalf_pos eq). have heq:= (BQps_sBQ hep). have [N NN HN]:=(sd _ hep). have[n [nN ha hb]]: exists n, [/\ inc n Nat, N <=c n & (Vg s n) <=q y -q e]. move: yb => [m ma mb]. move:(cmax_p1 (CS_nat ma)(CS_nat NN)); set q := cmax _ _. move => [ka kb]. have qN: natp q by apply:Gmax_E. ex_middle bad2; case: bad; exists q => // k kN lnk. have ha: ratp (Vg s k) by apply: BQ_seq_prop. have hb: inc (y -q Vg s k) BQp. apply/(qle_diffP ha ya); apply: mb => //; exact: (cleT ka lnk). rewrite /BR_seq_of_Q LgV// (BRdiff_cQ ha ya). rewrite (BRabs_cQ (QS_diff ha ya)) (BQabs_diff ha ya) (BQabs_pos hb). move: (BQp_sBQ hb) (BQps_sBQ eq) => su sv. apply/(rlt_cQ su sv);case: (qleT_el sv su) => // /(qle_diffP1 sv su). rewrite - (BQdiff_diff2 ya ha sv) BQsumC (BQdiff_diff2 ya sv ha). move /(qle_diffP1 ha (QS_diff ya sv)) => hd. case: bad2;exists k; split => //; exact: (cleT kb lnk). have [m [mN hm1 hm2]]: exists m, [/\ natp m, N <=c m & y -q (BQhalf e) <q (Vg s m)]. have hc:= (BQsum_Mps ya hep). case: (inc_or_not (y -q BQhalf e) A). move => /yc h; move/(BQsum_le2r ya (proj32 h) heq): h. rewrite (BQsum_diff1 heq ya) => hd; BQo_tac. have dq:=(QS_diff ya heq). move => bad2; ex_middle bad3; case bad2; apply:(Zo_i dq). exists N => // k ka kb;case:(qleT_el (BQ_seq_prop sa ka) dq) => // he. case: bad3; exists k; split => //. move:(proj1 (HN _ _ nN mN ha hm1)). move/(BQabs_prop1 (QS_diff (proj31 hb) (proj32_1 hm2)) heq) => [hc _]. move:(qlt_opp hm2); rewrite (BQoppB ya heq) => hd. move:(BQsum_Mlelt hb hd); rewrite - /(_ -q _). rewrite - {1} (BQdouble_half1 (BQps_sBQ eq))(BQdiff_diff2 ya heq heq). rewrite - (BQoppB ya heq) -/(_ -q _)(BQdiff_sum (proj31_1 hm2) (QSo heq)). move => he; BQo_tac. move => Ar1. have /BR_P Ar: real_dedekind A. split => //; [ apply:Zo_S | move => x xa; ex_middle u; case: Ar1]. exists x => // t ta; case:(qleT_el (Zo_S xa) (Zo_S ta)) => // tx. case:u;ex_tac. exists A => // e ep. move:(BQhalf_pos ep)(BQhalf_pos1 ep) => hep lt0. move:(sd _ hep) => [N NN Hn]; exists N => // n nN lenn. move/(rlt_cQ (proj31_1 lt0) (proj32_1 lt0)): lt0. apply: rle_ltT. have heq:=(BQps_sBQ hep). have xq:=(BQ_seq_prop sa nN). move: (RS_of_Q xq) (RS_of_Q heq) => xr er. rewrite /BR_seq_of_Q LgV//; apply/(BRabs_prop1 (RS_diff xr Ar) er). split. apply /(BRdiff_le2P xr Ar (RSo er)); rewrite /BRdiff (BRopp_K er). suff: inc (Vg s n +q (BQhalf e)) A. move => ha;rewrite (BRsum_cQ xq heq);apply:(proj1(BR_le_aux2 Ar ha)). apply/Zo_P; split; [ exact (QSs xq heq) | exists N => // k kN nk ]. have yq := (BQ_seq_prop sa kN). move/(BQabs_prop1 (QS_diff yq xq) heq):(proj1 (Hn _ _ kN nN nk lenn)). move => [_ hh]; move/(BQsum_le2l (proj31 hh) (proj32 hh) xq): hh. by rewrite (BQsum_diff xq (BQ_seq_prop sa kN)). apply/(BRdiff_le1P xr Ar er); rewrite (BRdiff_cQ xq heq). apply:(BR_le_aux3 Ar (QS_diff xq heq)) => /Zo_P [_ [m mN hm]]. move:(cmax_p1 (CS_nat mN)(CS_nat NN)); set q := cmax _ _. move => [ka kb]. have qN: natp q by apply:Gmax_E. have yq:= (BQ_seq_prop sa qN). move/(BQdiff_le2P xq heq yq):(hm _ qN ka) => hb. move/(BQabs_prop2 (QS_diff xq yq) heq):(Hn _ _ nN qN lenn kb). move => [_ h]; BQo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)