proposition: Lemma BQpair_irrational2 C: (BQpairL C \cup BQpairR C = BQ <-> forall x, ratp x -> exists2 n, natp n & (x <q P (Vg C n) \/ Q (Vg C n) <q x)).
proof: Proof. split => hb. move => x; rewrite / ratp - hb => /setU2_P [] /Zo_P [xq [n na nb]]. by exists n => //; left. by exists n => //; right. set_extens t; first by move/setU2_P => [] /Zo_S. by move => tq; move/hb: (tq) => [n nN] [] h; apply/setU2_P; [left | right]; apply/Zo_P; split => //; exists n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)