proposition: Lemma RIS_inv x: irrationalp x -> irrationalp (BRinv x).
proof: Proof. wlog xp: x/ inc x BRps. move => H xr. move /BR_P: (proj1 xr) => /BR_i1P; case => sx. + by case:(proj2(BR_of_Q_prop1 QS0)); rewrite -/BR_zero - sx. + by apply:H. + move: (H _ (BRopp_negative1 sx) (RSIo xr)). rewrite (BRinv_opp (BRms_sBR sx)) => /RSIo. by rewrite (BRopp_K (RS_inv (BRms_sBR sx))). move => xi. move:(RS_inv (BRps_sBR xp)) => /BR_P. rewrite (BRinv_irrational xi) (Y_true xp) => sa. split => // t /setC_P [tq h]. move:(xi) => [[pa pb pc pd pe] pf]. move: (BR_hi_Qps' xp) => [pa' _]. case/BQ_i2P: tq => tp; last first. move: pb => [u ux]; move:(pa' _ ux) => up; move:(QpsS_inv up) => iup. exists (BQinv u). apply/setC_P; split; first by apply:BQps_sBQ. move /setC_P => [_] []; apply/funI_P; ex_tac. move/ qge0xP: tp => sc; move/ qlt0xP: iup => sd; BQo_tac. have /funI_P[u ux ->]:inc t (fun_image x BQinv). ex_middle bad; case:h; apply/setC_P; split => //. move:(pe _ ux) => [v vx lt1];exists (BQinv v). move:(pa' _ vx) => vp; move:(QpsS_inv vp) => ivp. apply/setC_P; split; first by apply:BQps_sBQ. move => /setC_P [_] []; apply/funI_P; ex_tac. by apply/(BQinv_mon2 (pa' _ ux) (pa' _ vx)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)