proposition: Lemma continuous_inv x: realp x -> x <> \0r -> continuous_at BRinv x.
proof: Proof. move => xr xnz e ep. have ha: inc (BRabs x) BRps by apply: RpsSa. set e1 := BRhalf (BRabs x). have e1ps: inc e1 BRps by apply: BRhalf_pos. set e2 := e *r (BRabs x) *r e1. have e2ps: inc e2 BRps by exact: (RpsS_prod (RpsS_prod ep ha) e1ps). move:(rmin_prop2 e1ps e2ps) (rmin_prop1 (BRps_sBR e1ps) (BRps_sBR e2ps)). set e3:= (rmin e1 e2); move => sa [sb sc sd]; ex_tac => y [yr ya]. move: (RSa xr)(RSa yr) (proj32 sc) => axr ayr e1r. have hb: BRhalf (BRabs x) <=r BRabs y. move:(rle_triangular (RS_diff xr yr) yr); rewrite (BRsum_diff1 yr xr). move/(BRsum_le2r (proj31 ya) (proj32 sc) ayr):(rleT ya sc) => l1 l2. move:(rleT l2 l1); rewrite - {1} (BRdouble_half1 axr) -/e1 => l3. by apply/(BRsum_le2l e1r ayr e1r). have ynz: y <> \0r. move/ rlt0xP:e1ps => h1 h;move: hb; rewrite h BRabs_0 -/e1 => h2; BRo_tac. have pnz: x *r y <> \0r by apply: BRprod_nz. move: (RSp xr yr) (proj32 sd) => xyr e2r. have hc1: inc (BRabs (x *r y)) BRps by apply: RpsSa. have hc: inc (BRinv (BRabs (x *r y))) BRps by apply:RpsS_inv. move/BRps_iP: hc1 => [/BRp_sBR hca hcb]. move/(BRprod_ple2r (proj31 ya) e2r hc):(rleT ya sd). have hd: inc (e *r BRabs x) BRps by apply: RpsS_prod. move/ (BRprod_Mgt0le e1r ayr hd): hb. rewrite -/e2 -(BRprodA (BRps_sBR ep) axr ayr). rewrite - (BRprod_abs xr yr) => he. move: (BRprod_ple2r (proj31 he) (proj32 he) hc); rewrite (BRprodC e). rewrite -/(_ /r _) -/(_ /r _) (BRdiv_prod hca (BRps_sBR ep) hcb). rewrite (BRprodC _ e) => hf; move/hf: he => hg. move => eq;split; first by apply:RS_inv. rewrite (BRinv_diff xr yr xnz ynz) - (BRdiv_abs (RS_diff yr xr) xyr). rewrite (BRabs_diff yr xr); BRo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)