proposition: Lemma BRinv_opp x: realp x -> BRinv (BRopp x) = BRopp (BRinv x).
proof: Proof. move => xr. case/BR_rational_dichot: (xr) => rx. move/BR_of_Q_prop2: rx => [y yq ->]. move:(QSo yq) (QS_inv yq) => oyq iyq. rewrite (BRinv_Q yq) (BRopp_Q yq)(BRinv_Q oyq). by rewrite (BRopp_Q iyq) (BQinv_opp yq). rewrite (BRinv_irrational rx) (BRinv_irrational (RSIo rx)). case/BR_i2P: (xr) => h. move:(BRopp_positive1 h) => h2. by rewrite (Y_false (BR_di_neg_spos h2)) (Y_true h)(BRopp_K xr). case:(inc_or_not x BRps) => h1; first case:(BR_di_pos_neg h1 h). have xn:inc x BRms. apply/BRms_iP; split => // xe; case:(proj2(BR_of_Q_prop1 QS0)). by rewrite -/BR_zero - xe. move:(BRopp_negative1 xn) => h2. move:(BRps_sBR(RpsS_inv h2)); rewrite (BRinv_irrational (RSIo rx)). by rewrite (Y_true h2) (Y_false h1); move /BRopp_K => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)