proposition: Lemma BRsqrt_exists2 x (y := infimum BR_order (Zo BRp (fun z => x <=r BRsquare z))) : inc x BRp -> inc y BRp /\ x = BRsquare y.
proof: Proof. move:BR_osr => [or sr]. rewrite /y; set A := Zo _ _; clear y => xp; move: (BRp_sBR xp) => xr. have ha: sub A BR by move => t /Zo_S /BRp_sBR. have hd: sub A (substrate BR_order) by ue. have hb: nonempty A. have bp2 :=(BRps_sBRp RpsS1). have bp1:=(RpS_sum (RpS_square RS1)(RpS_square xr)). exists (\1r +r x); apply:Zo_i; first by apply:RpS_sum. rewrite (BRsum_square RS1 xr) (BRprod_1l xr) BRdouble_C -(BRdouble_s xr). rewrite (BRsumA (BRp_sBR bp1) xr xr) BRsumC. apply:(BRsum_Mp xr (RpS_sum bp1 xp)). have hc1: inc \0r BR /\ (forall y, inc y A -> gle BR_order \0r y). by split;[ exact:RS0 | move => t /Zo_S / rle0xP/BR_gleP]. have hc: bounded_below BR_order A by exists \0r;hnf;rewrite sr. move: (infimum_pr1 or (BR_inf_exists ha hb hc)). set y := (infimum BR_order A); move/(glbP or hd);rewrite /lower_bound. rewrite sr; move => [[sa sb] sc]. move: (sc _ hc1) => /BR_gleP / rle0xP y0; split; first exact. have yr := (BRp_sBR y0); have ysp:= (RpS_square yr); have ysr:=(BRp_sBR ysp). case: (equal_or_not x \0r) => xnz. have ww: BRsquare \0r = \0r by rewrite /BRsquare BRprod_0l. case: (equal_or_not y \0r) => ynz; first by rewrite xnz ynz ww. have yps: inc y BRps by apply /BRps_iP. case:(BR_di_pos_neg yps); apply / rge0xP /BR_gleP /sb /Zo_i => //; try ue. rewrite ww xnz; exact(rleR RS0). have xps: inc x BRps by apply /BRps_iP. have he:= continuous_square yr. case: (rleT_ell xr ysr) => // le. move /(rlt_diffP xr ysr): (le) => ep; move:(he _ ep) => [d dp de]. have dr := (BRps_sBR dp). case: (rleT_el yr dr) => le2. have ne1: BR_near y d \0r. hnf;rewrite (BRdiff_0r yr); split; [ exact:RS0 | by rewrite BRabs_pos]. move: (proj2(de _ ne1)); rewrite /BR_near /BRsquare BRprod_0r. rewrite (BRdiff_0r ysr) (BRabs_pos ysp) => /(BRdiff_le2P ysr xr ysr). by rewrite (BRdiff_xx ysr) => / rge0xP hi; case:(BR_di_pos_neg xps). have le3: inc (y -r d) BRp by apply/(rle_diffP dr yr); BRo_tac. have le4': y -r d <r y. by apply /(BRdiff_lt1P yr dr yr); rewrite (BRdiff_xx yr);apply/ rlt0xP. have le4:= (proj1 le4'). have dp':= (BRps_sBRp dp). have ne1: BR_near y d (y -r d). split => //; first by BRo_tac. rewrite (BRdiff_diff_simp yr dr) (BRabs_pos dp'); exact: rleR. have le5:= (BRsquare_mon1 le3 y0 le4). have d1r:= (proj31 le5); move/(rle_diffP d1r ysr): le5 => le6. move: (de _ ne1) => [sd]; rewrite (BRabs_pos le6). move/(BRsum_le2l (RSo d1r) (RSo xr) ysr) =>/(rle_oppP xr d1r) => h. have: inc (y -r d) A by apply: Zo_i. move /sb /BR_gleP => hf; BRo_tac. move /(rlt_diffP ysr xr): (le) => ep; move:(he _ ep) => [d dp de]. have dr := (BRps_sBR dp); have dr1 := (BRps_sBRp dp). have ydr':= (RpS_sum y0 dr1). have ydr:= (RSs yr dr). have le3':= (BRsum_Mps yr dp). case:(p_or_not_p (y +r d <=r y));[ by move/ rleNgt | case; apply/BR_gleP/sc]. split => // => t /Zo_P[tp ta]; apply /BR_gleP /(BRsquare_mon2 ydr' tp). have le4: BRabs d <=r d by rewrite (BRabs_pos dr1); apply:rleR. have le1: inc (BRsquare (y +r d) -r BRsquare y) BRp. apply/(rle_diffP ysr (RSp ydr ydr));apply:(BRsquare_mon1 y0 ydr'(proj1 le3')). have:(BR_near y d (y +r d)). split; [exact | by rewrite (BRabs_diff yr ydr) (BRdiff_sum yr dr) ]. move/de => [se]; rewrite (BRabs_diff ysr se) (BRabs_pos le1). move /(BRsum_le2r se xr (RSo ysr)) => sf; BRo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)