proposition: Lemma RpsS_inv x: inc x BRps -> inc (BRinv x) BRps.
proof: Proof. move => xp. case/BR_rational_dichot: (BRps_sBR xp) => rx. move: xp;move/BR_of_Q_prop2: rx => [y yq ->] h. rewrite (BRinv_Q yq); apply:RpsS_of_Q; apply: QpsS_inv. case/BQ_i2P: yq => // /RmS_of_Q hh; case: (BR_di_pos_neg h hh). rewrite (BRinv_irrational rx) (Y_true xp). set Y := (BQps -s fun_image x BQinv). move: rx => [[pa pb pc pd pe] pf]. move: (BR_hi_Qps' xp) => pa''. have yp1: forall y, inc y (BQps -s x) -> inc (BQinv y) Y. move => y /setC_P [yp ynx]; apply/Zo_P; split; first apply:(QpsS_inv yp). move /funI_P => [z za zb]; move:(BQinv_inj (BQps_sBQ yp)(pa _ za) zb) => h. by case: ynx; rewrite h. have yp2: forall y, inc y x -> inc (BQinv y) (BQps -s Y). move => y yx; apply/Zo_P; split;first exact:(QpsS_inv ((proj1 pa'') _ yx)). move /Zo_hi /funI_P ; case; ex_tac. have Yp: sub Y BQp by apply: sub_trans (BQps_sBQp); apply: Zo_S. apply/BRps_iP; split; last first. move: pb => [u0 /yp2 u0x] eq; move: u0x. rewrite eq - BRzero_prop setC_v; case; case. apply:Zo_i; [apply/BR_P; split | exact: Yp]. + apply:(sub_trans Yp BQp_sBQ). + move:(setC_ne pa'') => [u /yp1 yy]; ex_tac. + move => hc;rewrite hc in Yp. by move:(BQ_di_neg_pos QmsSm1); apply; apply: Yp QSm1. + move => a b /setC_P [ap aby] lab. have bp: inc b BQps by move/ qlt0xP: ap => ap; apply/ qlt0xP; BQo_tac. apply/setC_P;split => //. move:(BQinv_K (BQps_sBQ ap)) => eq1. move => /funI_P [c cx bv]; case: aby; apply /funI_P; exists (BQinv a) => //. apply:(pd _ _ cx). move /(BQprod_Mlt1 (BQps_sBQ ap) bp): lab. rewrite bv /BQdiv (BQinv_K (pa _ cx)) BQprodC => H. by apply/(BQprod_Mlt1 (pa _ cx) (QpsS_inv ap)); rewrite /BQdiv eq1. + move => y /Zo_P [ya yb]; move: (BQps_sBQ ya) => yq. move: (QpsS_inv ya)(BQinv_K yq) => yc yd. have /pf [z /setC_P[za zb] zc]: inc (BQinv y) (BQ -s x). by apply/setC_P; split; [ apply:QS_inv | dneg w; apply/funI_P; ex_tac]. have zp:inc z BQps by move/ qlt0xP: yc => yc; apply/ qlt0xP;BQo_tac. exists (BQinv z); first by apply: yp1; apply/setC_P. move:(BQps_nz ya)(BQps_nz zp) => ynz znz. move:(BQprod_Mltgt0 (QpsS_inv zp)(BQprod_Mltgt0 ya zc)). rewrite BQprodC (BQprodC _ y) (BQprod_inv1 yq ynz) (BQprod_1r (QS_inv za)). by rewrite -/((z *q y) /q z) (BQdiv_prod za (BQps_sBQ ya) znz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)