proposition: Lemma square_root_cv1 a b (f := fun z => (BRsquare z +r a) /r (\2r *r z)) (seq:= induction_defined f b) (xn := Lg Nat (Vf seq)) (x := infimum BR_order (range xn)): inc a BRp -> \1r +r a <=r b -> [/\ inc x BRp, limitR xn x & BRsquare x = a].
proof: Proof. move => pa pb. have ar: realp a by apply:BRp_sBR. have tp2:= (BRps_sBRp RpsS2). move: (BRsqrt_exists pa) => [c cp cs]. have cr: realp c by apply:BRp_sBR. have fz: f \0r = \0r by rewrite /f /BRdiv BRprod_0r BRinv_0 BRprod_0r. move: RS2 BR2_nz => rs2 r2z. have cp1: forall t, c <=r t -> inc t BRp. move => t lt; apply / rle0xP; move/ rle0xP: cp => sa;BRo_tac. have cp2: forall t, c <=r t -> inc (\2r *r t) BRp. move => t /cp1 tr;apply (RpS_prod tp2 tr). have comp_c: forall t, inc t BRp -> a <=r (BRsquare t) -> c <=r t. rewrite cs; move => t tp h; case: (rleT_el cr (BRp_sBR tp)) => // h2. move: (BRprod_Mltltge0 tp tp h2 h2) => h'; BRo_tac. have nr: forall t, realp t -> inc (BRsquare t +r a) BRp. move => t tr; exact (RpS_sum (RpS_square tr) pa). have hc: forall t, c <=r t -> inc (BRsquare t -r a) BRp. move => t lct; move: (proj32 lct) => tr. apply / rle0xP;apply/ (rle_diffP1 ar (RSp tr tr)); rewrite cs. apply: (BRprod_Mlelege0 (cp1 _ lct) cp lct lct). have ha: forall t,inc t BR -> t -r (f t) = (BRsquare t -r a) /r (\2r *r t). move => t tr; case: (equal_or_not t \0r) => tnz. by rewrite tnz fz /BRdiv BRprod_0r BRinv_0 BRprod_0r (BRdiff_0r RS0). have pnz: \2r *r t <> \0r by apply: BRprod_nz. rewrite /f (BRdiff_div tr (BRp_sBR (nr _ tr)) (RSp RS2 tr) pnz). rewrite (BRprodC \2r) BRprodA // - (BRdouble_s (RSp tr tr)) (BRsumC _ a). by rewrite BRdiff_sum_simpl_r //; apply:RSp. have hb: forall t, realp t -> inc (f t) BR. move => t tr; apply:(RS_div (BRp_sBR (nr _ tr))) (RSp rs2 tr). rewrite /f /BRsquare. have hd: forall t, c <=r t -> inc (f t) BRp. move => t ct; apply: (RpS_div (nr _ (proj32 ct)) (cp2 _ ct)). have he:(forall t, c <=r t -> f t <=r t). move => t lct; have tr:= (proj32 lct). apply/ (rle_diffP1 (hb _ tr) tr); rewrite (ha _ tr); apply/ rle0xP. apply /(RpS_div (hc _ lct) (cp2 _ lct)). have hf:(forall t, c <=r t -> c <=r f t /\ f t <=r t). move => t lct; move:(proj32 lct) => tr; split; last by apply: he. apply: (comp_c _ (hd _ lct)). have str: realp (BRsquare t) by apply:RSp. have ra: realp (BRsquare t +r a) by apply:RSs. have rb:= (RSp RS2 tr). case: (equal_or_not t \0r) => tnz. move: lct cs; move/ rle0xP:cp; rewrite tnz fz => sa sb. rewrite (rleA sb sa) => ->; rewrite /BRsquare (BRprod_0r); BRo_tac. have rc: inc t BRps by apply/BRps_iP;move: (cp1 _ lct). set v := (BRsquare (BRsquare t +r a /r \1r)). have vv: v = (BRsquare (BRsquare t +r a)) by rewrite /v (BRdiv_x1 ar). have vr: realp v by rewrite vv; apply:RSp. have rd:= (RpsS_prod RpsS2 rc). have re:=(RpsS_prod rd rd). rewrite /f (BRdiv_square ra rb) -(BRdiv_x1 ar). apply /(BRdiv_Mlelege0 ar RpsS1 vr re); rewrite (BRprod_1l vr) vv. rewrite (BRprod_ACA RS2 tr RS2 tr) (BRsumdiff_square (RSp tr tr) ar). rewrite BRprod_22 BRprodC -/(BRsquare t) (BRprodA RS4 str ar). exact (BRsum_Mp (RSp (RSp RS4 str) ar) (RpS_square (RS_diff str ar))). have lcb: c <=r b. have bp1:= (rleT (BRsum_Mp RS1 pa) pb). have bp2 :=(BRps_sBRp RpsS1). move: (BRsum_Mp ar bp2); rewrite BRsumC=> bp3;move:(rleT bp3 pb) => bp4. have bp:inc b BRp by apply / rle0xP; move/ rle0xP: bp2 => h; BRo_tac. apply:comp_c => //. by move:(BRprod_Mlelege0 bp pa bp1 bp4);rewrite (BRprod_1l ar). move: (induction_defined_pr f b) => []; rewrite -/seq => ua uvb uc ud. have hi: BR_seq xn. apply: BR_seq_prop1; apply: Nat_induction. by rewrite uc; exact(proj32 lcb). by move => n nN h; rewrite ud //; apply: hb. have hj: forall n, natp n -> c <=r Vg xn n /\ Vg xn (csucc n) <=r Vg xn n. move => n nN; move: (NS_succ nN) => snN;rewrite /xn !LgV//. clear snN; move: n nN; apply: Nat_induction. by rewrite (ud _ NS0) uc; split => //; apply: he. move => n nN [h1 h2]; move:(proj1 (hf _ h1)); rewrite - (ud _ nN) => h3. by split => //;rewrite (ud _ (NS_succ nN)); apply: he. have hk:(forall n, natp n -> c <=r Vg xn n) by move => t /hj []. have hl:(forall n, natp n -> Vg xn (csucc n) <=r Vg xn n) by move => t /hj []. move:(decreasing_bounded_limit hi hk hl);rewrite -/x; move => [cxr lx]. clear hi hj hk hl. case: (equal_or_not x \0r) => xnz. split => //; [by rewrite xnz; apply: RpS0 | rewrite cs xnz ]. have -> //: c = \0r by apply:rleA; [ue | apply/ rle0xP]. move: (proj32 cxr) => xr. have hg: f x = x -> BRsquare x = a. move => eq;move: (ha _ xr); rewrite eq (BRdiff_xx xr) => /esym h. case: (equal_or_not (BRsquare x -r a) \0r) => h1. by apply: (BRdiff_xx_rw (RSp xr xr) ar). have ra: realp (BRsquare x -r a) by apply: RS_diff => //; apply: RSp. have rb: realp (\2r *r x) by apply:RSp. have rc: (BRinv (\2r *r x)) <> \0r. by move => /(BRinv_eq0 rb); apply: BRprod_nz. by case: (BRprod_nz ra (RS_inv rb) h1 rc). 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) ar)). apply: (continuous_div xr p1 (continuous_comp p2 ra)). exact: (proj1(continuous2_prod RS2 xr)). move:(decreasing_limit_bounded_fix hf lcb cfx) => []. by rewrite -/seq -/xn -/x => Ra /hg Rb Rc; split => //; apply: cp1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)