proposition: Lemma BRsqrt_exists x: inc x BRp -> exists2 y, inc y BRp & x = BRsquare y.
proof: Proof. move => xr. have ha: \0r <=r x by apply / rle0xP. have hb: BRsquare \0r <=r x by rewrite /BRsquare BRprod_0r. have [y xy fy]: exists2 y, \0r <=r y & x <=r BRsquare y. case: (rleT_ee (BRp_sBR xr) RS1) => h. exists \1r; first by apply/ rle0xP; exact:(BRps_sBRp RpsS1). by rewrite /BRsquare (BRprod_1r RS1). by exists x => //; move:(BRprod_Mlege0 xr h);rewrite (BRprod_1l (proj32 h)). have hc: (forall z, \0r <=r z -> z <=r y -> continuous_at BRsquare z). by move => z [_ za _] _; move:(continuous_square za). have hd:(BR_between x (BRsquare \0r) (BRsquare y)) by left. move:(Bolzano2 xy (Bolzano_hyp_simp xy hc) hd) => [z [/ rle0xP za _] zb]. ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)