proposition: Lemma rle_opp x y: x <=r y -> (BRopp y) <=r (BRopp x).
proof: Proof. move => [xr yr lexy]; split;try apply:RSo => //. case/BR_rational_dichot:xr => rx; case/BR_rational_dichot:yr => ry. + move:lexy;move/BR_of_Q_prop2: rx => [x' x'q ->]. move/BR_of_Q_prop2: ry => [y' y'q ->] H. have ha: x' <=q y'. by apply /(rle_cQ x'q y'q); split => //; apply:RS_of_Q. move:(qle_opp ha) => /(rle_cQ (QSo y'q) (QSo x'q)) [_ _]. by rewrite !BRopp_Q. + move:lexy;move/BR_of_Q_prop2: rx => [x' x'q ->]; rewrite BRopp_Q //. rewrite (BRopp_irrational ry) => lexy. move => t /Zo_P [tq ha]; move: (qlt_opp ha); rewrite (BQopp_K x'q) => hb. apply/funI_P; exists (BQopp t); last by rewrite (BQopp_K tq). apply/setC_P; split; [by apply:QSo | move => ty]. move:(lexy _ ty) => /Zo_hi [hc _]; BQo_tac. + move:lexy;move/BR_of_Q_prop2: ry => [y' y'q ->]; rewrite BRopp_Q //. rewrite (BRopp_irrational rx)=> lexy. move => t /funI_P [z /setC_P [za zb] ->]; apply:Zo_i;first by apply:QSo. case: (qleT_ell y'q za). - move => eq; case: zb; rewrite - eq; ex_middle nyx. move:(rx) => [_ irx]. move:(irx _ (setC_i y'q nyx)) => [v /setC_P [va vb] vc]. by case:vb; apply:lexy; apply/Zo_i. - by move => ha; case: zb; apply: lexy; apply /Zo_P. - by move/ qlt_opp. + rewrite (BRopp_irrational rx) (BRopp_irrational ry). move => t /funI_P [z /setC_P[za zb] ->]; apply /funI_P; exists z => //. by apply/setC_P; split => //; dneg h; apply: lexy. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)