proposition: Lemma BRopp_K x: realp x -> BRopp (BRopp x) = x.
proof: Proof. case/BR_rational_dichot => rx. move/BR_of_Q_prop2: rx => [y yq ->]. by rewrite (BRopp_Q yq) (BRopp_Q (QSo yq)) (BQopp_K yq). move:(RSIo rx). rewrite (BRopp_irrational rx) => h; rewrite (BRopp_irrational h). set_extens t. move => /funI_P [z /setC_P [za zb] ->]; ex_middle k; case: zb. have sc:=(QSo za). apply/funI_P; exists (BQopp z); [ by apply/setC_P | by rewrite BQopp_K]. move => tx; move:(rx) => [[ha _ _ _ _] _]; move:(ha _ tx) => tq. apply /funI_P; exists (BQopp t); last by rewrite BQopp_K. apply/setC_P; split; first by apply:QSo. move /funI_P => [z /setC_P [za zb]]. by move/(BQopp_inj tq za) => eq;case:zb; rewrite - eq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)