proposition: Lemma BR_of_Q_prop2 X: rationalp X -> exists2 x, ratp x & X = BR_of_Q x.
proof: Proof. move => [pu pf]; ex_middle h; case: pf; split => // x /setC_P [xq nxX]. move:pu => [pa pb pc pd pe]. ex_middle h2;case: h; exists x => //. have ha: forall y, inc y (BQ -s X) -> y <=q x. move => y yu;move/setC_P: (yu) => [yq _]. case:(qleT_el yq xq) => // h; case: h2; ex_tac. set_extens t. move => tx; apply/Zo_P; split => //; first by apply: pa. case:(qleT_el (pa _ tx) xq) => // tb;case: nxX. by case: (equal_or_not t x) => etx; [rewrite - etx | apply:(pd _ _ tx)]. move => /Zo_P [tq xt]; ex_middle tne; move:(ha _ (setC_i tq tne)) => hb. BQo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)