proposition: Lemma square_root_cv3 a b (f := fun z => (BRsquare z +r a) /r (\2r *r z)) (g := fun z => BRhalf ((f z) +r z)) (s := BRsqrt a) (seq:= induction_defined g b) (xn := Lg Nat (Vf seq)) (x := supremum BR_order (range xn)): inc a BRp -> (s /r \3r) <=r b -> b <=r s -> [/\ inc x BRp, limitR xn x & x = s].
proof: Proof. move => pa pb pc. move:(square_root_cv2 pa) => [ha hb hc hd]. move: (BRsqrt_prop pa); rewrite -/s; move => [sa sb]. have sp: \0r <=r s /r \3r by apply/ rle0xP;exact(RpS_div sb (BRps_sBRp RpsS3)). have srr := (BRp_sBR sb). have bp: inc b BRp by apply / rle0xP; BRo_tac. set B := Zo BR (fun z => s /r \3r <=r z /\ z <=r s). have bb: inc b B by apply:Zo_i; [ apply:BRp_sBR | done ]. have Bp: forall z, inc z B -> inc (g z) B. move => z /Zo_P [szr [za zb]]; move:(hd _ za zb) => zc. move:(rleT za (hc _ (rleT sp za) zb)) => sd. apply: Zo_i => //; exact:(proj32 sd). move: (induction_defined_pr g b) => []; rewrite -/seq => ua ub uc ud. have qa: fgraph xn by rewrite /xn; fprops. have qb: domain xn = Nat by rewrite /xn;aw. have srb: sub (range xn) B. move => t /(range_gP qa); rewrite qb; move => [n nN ->]; rewrite /xn LgV//. move: n nN ; apply: Nat_induction; first ue. by move => n nN h; rewrite (ud _ nN); apply: Bp. have he: sub (range xn) BR by move => t /srb /Zo_S. have Vseq: forall n, natp n -> Vg xn n = Vf seq n. move => n nN; rewrite /xn LgV//. have seqz: forall n, natp n -> inc (Vg xn n) B. move => n nN; apply: srb;apply/(range_gP qa);rewrite qb; exists n; fprops. have seqx: BR_seq xn by split. have seqy:forall n, natp n -> Vg xn n <=r s by move => n /seqz /Zo_P [_ []]. have seqt: (forall n, natp n -> Vg xn n <=r Vg xn (csucc n)). move => n nN; move: (seqz _ nN) => /Zo_hi []. rewrite (Vseq _ nN) (Vseq _ (NS_succ nN)) (ud _ nN) => p1 p2. apply: hc => //; BRo_tac. move:(increasing_bounded_limit seqx seqy seqt) => [];rewrite -/x => Ha Hb. move:BR_osr => [or sr]. have he': sub (range xn) (substrate BR_order) by rewrite sr. have hf': inc (Vg xn \0c) (range xn). by apply/(range_gP qa); rewrite qb; exists \0c => //; apply: NS0. have hf: nonempty (range xn) by ex_tac. have hg: bounded_above BR_order (range xn). by exists s; split; [ue | move => y /srb /Zo_hi [_] /BR_gleP]. move: (supremum_pr1 or (BR_sup_exists he hf hg)); rewrite -/x. move/(lubP or he');rewrite /upper_bound sr;move=> [[xr hj] hk]. have hl': (Vg xn \0c) = b by rewrite /xn LgV//; apply: NS0. have hl: s /r \3r <=r x by apply /(rleT pb) /BR_gleP / hj; rewrite - hl'. have xp: inc x BRp by apply / rle0xP;exact: (rleT sp hl). case: (equal_or_not x \0r) => xnz. rewrite xnz in hl; move:(rleA hl sp) => /(BRprod_nz_bis srr (RS_inv RS3)). case; first by move => ->;split => //; rewrite xnz; apply:RpS0. by move/(BRinv_eq0 RS3) => h; case: (BRps_nz RpsS3). have xpp: inc x BRps by apply setC1_P. move: RS2 BR2_nz (BRps_sBRp RpsS2) => rs2 r2z tp2. have cfx: continuous_at f x. have p1: \2r *r x <> \0r by apply: BRprod_nz. have p2:=(continuous_prod xr (continuous_id xr) (continuous_id xr)). have ra := (proj2 (continuous2_sum (RSp xr xr) (BRp_sBR pa))). apply: (continuous_div xr p1 (continuous_comp p2 ra)). exact: (proj1(continuous2_prod RS2 xr)). have cgx: continuous_at g x. have p2:= (continuous_sum xr cfx (continuous_id xr)). have p3:= (RS_div (RSs (RSp xr xr) (BRp_sBR pa)) (RSp rs2 xr)). exact:(continuous_comp p2 (proj2(continuous2_prod (RSs p3 xr) RSh2))). move: (limit_of_continuous_fix_pos hb bp cgx Hb xr) => [ea eb]. move:(proj1 (ha _ xr xnz) ea); case => xs; first done. case: (BR_di_pos_neg xpp); rewrite xs; exact: (BRopp_positive2 sb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)