proposition: Lemma BRprod_inv1 x : realp x -> x <> \0r -> (x *r (BRinv x)) = \1r.
proof: Proof. wlog xp:x /(inc x BRps). move => H xq xns;case /BR_i1P:(xq) => xs //; first by apply:H. move: (BRopp_negative1 xs) => oxp; move:(BRps_sBR oxp) => oxr. rewrite -(BRprod_opp_opp xq (RS_inv xq)) - (BRinv_opp xq); apply: H => //. by move /BRps_iP:oxp => [_ ]. case/BR_rational_dichot => rx. move/BR_of_Q_prop2: rx => [y yq ->] h. rewrite (BRinv_Q yq) (BRprod_cQ yq (QS_inv yq)) (BQprod_inv1) //. by dneg h1; rewrite h1. move => _. rewrite (BR_prod_aux1 xp (RpsS_inv xp)). rewrite (BRinv_irrational rx)(Y_true xp). move:(rx) => [[pa pb pc pd pe] pf]. set_extens t. move/BR_prod_auxP => [z zx [u /setC_P [up uix] ->]]. suff h: \1q <q z *q u. apply/Zo_P; split => //; exact:(proj32_1 h). move:(BRi_sQ (BRps_sBR xp) zx) => zq. have uq:= (BQps_sBQ up). have unz:= (BQps_nz up). have uiq:= QS_inv uq. apply/(BQprod_plt2r QS1 (QSp zq uq) (QpsS_inv up)). rewrite (BQprod_1l uiq) -/(_ /q _) BQprodC BQdiv_prod //. case:(qleT_el zq uiq) => // zu; case: uix. apply/funI_P;exists (BQinv u); last by rewrite BQinv_K. case: (equal_or_not (BQinv u) z) => uz; first by rewrite uz. apply: (pd _ _ zx (conj zu (nesym uz))). move => /Zo_P[tq t1]; apply/BR_prod_auxP. have tp: inc t BQps. by have lt01:=qlt_01; apply/ qlt0xP; BQo_tac. have[w wx wp]: exists2 w, ~inc w x & \0q <q w. move:(setC_ne (BR_hi_Qps' xp)) => [w /setC_P [/ qlt0xP sa sb]]. by exists w. set delta := w *q (\1q -q BQinv t). have itq:=(QS_inv tq). have itp: inc (\1q -q BQinv t) BQps. apply / qlt0xP/ (qlt_diffP1 itq QS1). by move/(BQinv_mon2 tp QpsS1): t1; rewrite BQinv_1. have dp: inc delta BQps by apply:QpsS_prod; [ apply/ qlt0xP | ]. have [y yx yv] := (BRi_lowbound (BRps_sBR xp) dp). have yq := (pa _ yx). have yp:= (BR_hi_Qps (BRps_sBRp xp) yx). have ynz:=BQps_nz yp. exists y => //; exists (t /q y); last by rewrite BQprod_div. apply/setC_P; split;first by apply:QpsS_div. move => /funI_P [z zx zv]. case: (qleT_ell (BQps_sBQ yp) (proj32_1 wp)) => wy. by case: wx; rewrite - wy. case: wx; apply:(pd _ _ yx wy). move /(BQprod_Mltgt0 itp): wy; rewrite -/delta. rewrite (BQprodBr yq QS1 itq) (BQprod_1r yq). rewrite -/(_ /q _)-(BQinv_div tq yq) zv (BQinv_K (pa _ zx)) => la. move/(BQsum_lt2r (proj31_1 la)(proj32_1 la) (pa _ zx)): la. rewrite (BQsum_diff1 (pa _ zx) yq) => lb. have lc:=(yv _ zx). move/(BQsum_lt2l (proj31_1 lc)(proj32_1 lc) (BQps_sBQ dp)): lc. rewrite (BQsum_diff (BQps_sBQ dp) yq); move => [ld _]; BQo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)