proposition: Lemma BQpair_rational C : BQpair C -> BQpair_aux3 C -> exists2 x, ratp x & BQpairR C = BR_of_Q x.
proof: Proof. move => Hab Hc. move: Hc => [t tv]. move:(set1_1 t); rewrite - tv; move => /setC_P [tq ta]. exists t => //; set_extens u. move => /Zo_P [uq [n nN nv]]; apply /Zo_P; split => //. case: (qleT_el tq (proj31_1 nv)) => h; first by BQo_tac. by case: ta; apply/setU2_P; right; apply:Zo_i => //; exists n. move => /Zo_P [uq ltu]. case: (inc_or_not u (BQpairL C \cup BQpairR C)) => ha; last first. have: inc u (singleton t) by rewrite - tv; apply/setC_P. by move/set1_P => ut; case:(proj2 ltu); rewrite ut. case/setU2_P: ha => // /Zo_P [_ [n nN nv]]. by case: ta; apply/setU2_P; left; apply:Zo_i => //; exists n => //; BQo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)