proposition: Lemma RSo x: realp x -> realp (BRopp x).
proof: Proof. case/BR_rational_dichot => rx. move/BR_of_Q_prop2: rx => [y yq ->]. rewrite (BRopp_Q yq);apply:(RS_of_Q (QSo yq)). rewrite (BRopp_irrational rx); apply /BR_P. move: rx => [[pa pb pc pd pe] pf]. split. + by move => t /funI_P [z /setC_P [za _] ->]; apply: QSo. + apply: funI_setne; exact:(setC_ne (conj pa pc)). + move => eq; move:(pb) => [y yx]. move:(QSo (pa _ yx)); rewrite /ratp - eq. move /funI_P => [z /setC_P [za zb] eq2]. by case: zb; rewrite - (BQopp_inj (pa _ yx) za eq2). + move => a b /funI_P [z /setC_P [za zb] ->] h. move:(qlt_opp h); rewrite (BQopp_K za) => h1; move: (proj31_1 h1) => xx. apply/funI_P; exists (BQopp b). apply/setC_P; split => // h2; case: zb; exact:(pd _ _ h2 h1). by rewrite(BQopp_K (proj32_1 h)). + move => a /funI_P [z /pf [y /setC_P [ya yb yc]] ->]. exists (BQopp y); first by apply/funI_P; exists y => //; apply/setC_P. apply:(qlt_opp yc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)