proposition: Lemma BRinv_K x: realp x -> BRinv (BRinv x) = x.
proof: Proof. wlog xp: x / inc x BRps. move => H xr; case /BR_i1P:(xr) => sx. + by rewrite sx !BRinv_0. + by apply:H. + move:(RSo xr) => h. move: (f_equal BRopp (H _ (BRopp_negative1 sx) h)). by rewrite - (BRinv_opp (RS_inv h)) - (BRinv_opp h) (BRopp_K xr). case/BR_rational_dichot => rx. move/BR_of_Q_prop2: rx => [y yq ->]. by rewrite (BRinv_Q yq) (BRinv_Q (QS_inv yq)) (BQinv_K yq). move:(RpsS_inv xp) (RIS_inv rx). rewrite (BRinv_irrational rx) => ha h; rewrite (BRinv_irrational h). rewrite (Y_true ha) (Y_true xp); clear h ha. set_extens t. move => /setC_P[tp h];ex_middle tnx; case:h. have e1 :=(BQinv_K (BQps_sBQ tp)). apply/funI_P; rewrite - e1; exists (BQinv t) => //. apply/setC_P; split; [ apply: (QpsS_inv tp) | move => /funI_P [z zx zv]]. by case: tnx; rewrite (BQinv_inj (BQps_sBQ tp) (BRi_sQ (BRps_sBR xp) zx) zv). move => tx; move:((proj1 (BR_hi_Qps' xp)) _ tx) => tp. apply/setC_P; split =>// /funI_P [ z /setC_P [za zb] zc]; case: zb. by apply/funI_P; ex_tac; rewrite zc (BQinv_K (BQps_sBQ za)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)