proposition: Lemma square_root_cv2 a (f := fun z => (BRsquare z +r a) /r (\2r *r z)) (g := fun z => BRhalf ((f z) +r z)) (s := BRsqrt a): inc a BRp -> [/\ forall x,realp x -> x <> \0r -> (g x = x <-> x = s \/ x = BRopp s), (forall x, inc x BRp -> inc (g x) BRp), (forall x, \0r <=r x -> x <=r s -> x <=r (g x)) & (forall x, (s /r \3r) <=r x -> x <=r s -> g x <=r s)].
proof: Proof. move => pa; move: (BRp_sBR pa) => ra. have fz: f \0r = \0r by rewrite /f /BRdiv BRprod_0r BRinv_0 BRprod_0r. move: RS2 BR2_nz (BRps_sBRp RpsS2) => rs2 r2z tp2. have nr: forall t, realp t -> inc (BRsquare t +r a) BRp. move => t tr; exact (RpS_sum (RpS_square tr) pa). have ha: forall t, realp t -> 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 -> realp (f t). move => t tr; apply:(RS_div (BRp_sBR(nr _ tr)) (RSp rs2 tr)). have hc: forall t, inc t BRp -> inc (f t) BRp. move => t tp; apply: (RpS_div (nr _ (BRp_sBR tp)) (RpS_prod tp2 tp)). have hd: forall t, inc t BRp -> inc (g t) BRp. move => t tp; exact: (RpS_prod (RpS_sum (hc _ tp) tp) (BRps_sBRp RpsSh2)). have he: forall t, realp t -> realp (g t). move => t tr; exact:(RSp (RSs (hb _ tr) tr) RSh2 ). have hf: forall t, realp t -> t -r g t = BRhalf(t -r f t). move => t tr. rewrite /g BRhalf_prop (BRdiff_div tr (RSs (hb _ tr) tr) rs2 r2z). by rewrite -(BRdouble_s tr) (BRdiff_sum_simpl_r tr (hb _ tr) tr) BRhalf_prop. have hg: forall x, realp x -> (g x = x <-> x -r f x = \0r). move => x xr; split => h; move:(hf _ xr); rewrite h? (BRdiff_xx xr). move /esym/(BRprod_nz_bis (RS_diff xr (hb _ xr)) RSh2); case => // h0. by case:(BRps_nz RpsSh2). by rewrite /BRhalf BRprod_0l; move/(BRdiff_xx_rw xr ((he _ xr))). move: (BRsqrt_prop pa); rewrite -/s; move => [sa sb]. have sr := (BRp_sBR sb). have hi:forall x, realp x -> x <> \0r -> (g x = x <-> x = s \/ x = BRopp s). move => x xr xnz; move:(hg _ xr); rewrite (ha _ xr) sa => ww. have qe: realp (BRsquare s) by apply:RSp. split. have qd:realp (BRsquare x) by apply:RSp. have qa:realp (BRsquare x -r BRsquare s) by apply:RS_diff. have qb:realp(BRinv (\2r *r x)) by apply:(RS_inv (RSp rs2 xr)). move/ww/(BRprod_nz_bis qa qb); case. by move/(BRdiff_xx_rw qd qe)/(BRsquare_inj xr (BRp_sBR sb)). move/(BRinv_eq0 (RSp rs2 xr)) /(BRprod_nz_bis RS2 xr); case => //. move/(BRsquare_inj xr sr ) => sx; apply /ww. by rewrite sx (BRdiff_xx qe) /BRdiv BRprod_0l. have hj:forall x, \0r <=r x -> x <=r s -> x <=r g x. move => x / rle0xP xp le1; move:(BRp_sBR xp) => xr. apply /(rle_diffP2 xr (he _ xr)); rewrite (hf _ xr) /BRhalf BRprodC. apply:(RpmS_prod (BRps_sBRp RpsSh2)); rewrite (ha _ xr). apply:BRmpS_div (RpS_prod tp2 xp); rewrite sa (BRsquare_diff xr sr) BRprodC. by apply:(RpmS_prod (RpS_sum xp sb)); apply /(rle_diffP2 xr sr). split => //. move => x le1 le2. case: (equal_or_not s \0r) => snz. move:le1 le2; rewrite snz BRdiv_0x => le1 le2. rewrite /g /f (rleA le2 le1) (BRprod_0r) BRdiv_x0 (BRsum_0r RS0). rewrite /BRhalf(BRprod_0l); apply: (rleR RS0). have spp: inc s BRps by apply/BRps_iP. have xpp: inc x BRps. apply/ rlt0xP; apply: rlt_leT le1; apply/ rlt0xP;exact:(RpsS_div spp RpsS3). have xnz:=(BRps_nz xpp). have xr: realp x by BRo_tac. have pb: realp (BRsquare x) by apply:RSp. have pc: realp (BRsquare x +r a) by apply:RSs. have pd: realp (\2r *r x) by apply:RSp. have pe: \2r *r x <> \0r by apply: BRprod_nz. have ar := (BRp_sBR pa). have pf:=(RSs (RSp RS3 pb) ar). have gv: g x = (\3r *r BRsquare x +r a) /r (\4r *r x). rewrite /g/f BRsumC (BRsum_div xr pc pd pe) (BRprodC x) -(BRprodA RS2 xr xr). rewrite -/(BRsquare x) (BRsumA (RSp rs2 pb) pb ar). rewrite -{2} (BRprod_1l pb) - (BRprodDl pb rs2 RS1) BR_plus21 BRhalf_prop. rewrite /BRdiv - (BRprodA pf (RS_inv pd)(RS_inv rs2)) - (BRprod_inv pd rs2). rewrite(BRprodC _ \2r) (BRprodA rs2 rs2 xr) BRprod_22//. have isr := proj32 le2. have qa:= (RS_diff (RSp RS3 xr) isr). have qb:= (RS_diff xr isr). have qc':= (RpsS_prod RpsS4 xpp). have qc:= (RSp RS4 xr). have qd := RS_div (RSp qa qb) qc. suff gv1: g x = s +r ((\3r *r x -r s) *r ( x -r s)) /r (\4r *r x). rewrite gv1; apply: (BRsum_Mm isr); apply: BRmpS_div (BRps_sBRp qc'). apply: RpmS_prod; last by apply/ rle_diffP2. move:(BRps_nz RpsS3) (BRps_sBRp RpsS3) => qe qf. rewrite - (BRprod_div RS3 sr qe) - (BRprodBr RS3 xr (RS_div sr RS3)). by apply: (RpS_prod qf); apply/ (rle_diffP (proj31 le1) xr). have rs3 := RS3. have pxs := RSp xr sr. move: (RSp RS3 pb)(RSp RS3 pxs)(RSp sr sr)(RSp RS4 pxs) => p3xx p3xs pss p4xs. have qe: realp (\3r *r (x *r x) -r x *r s) by exact (RS_diff p3xx pxs). rewrite (BRsum_div sr (RSp qa qb) qc (BRps_nz qc')) gv; congr (_ /r _). rewrite sa (BRprodBr qa xr sr) (BRprodDl xr (RSp RS3 xr) (RSo sr)). rewrite (BRprodDl sr (RSp RS3 xr) (RSo sr)) -! BRopp_prod_l //. rewrite - (BRprodA rs3 xr xr) - (BRprodA rs3 xr sr) (BRprodC s x). rewrite -/(_ -r _) (BRdiff_diff qe p3xs pss) (BRdiff_diff2 p3xx pxs p3xs). rewrite -{1} (BRprod_1l pxs) - (BRprodDl pxs RS1 RS3) (BRsumC \1r)BR_plus31. rewrite (BRprodC s) - (BRprodA RS4 xr sr). by rewrite (BRsumA p4xs (RS_diff p3xx p4xs) pss) (BRsum_diff p4xs p3xx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)