proposition: Lemma RSIo x: irrationalp x -> irrationalp (BRopp x).
proof: Proof. move => xi. have ra:=(BRopp_irrational xi). move: (xi) => [xr pf]; move:(xr) => [pa pb pc pd pe]. split; first by move/BR_P:(xr) => /RSo /BR_P. move => a /setC_P [aq nax]. have: inc (BQopp a) x. ex_middle h;case: nax; rewrite ra; apply/funI_P; exists (BQopp a). by apply/setC_P; split => //; apply:QSo. by rewrite (BQopp_K aq). move/pe => [y yx lya]; move:(qlt_opp lya); rewrite (BQopp_K aq) => la. exists (BQopp y) => //; apply/setC_P; split;first exact:(proj32_1 la). rewrite ra; move/funI_P => [z /setC_P[za zb]] /(BQopp_inj (proj31_1 lya) za). by move => eq; case: zb; rewrite - eq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)