proposition: Lemma BQpair_irrational C: BQpair C -> (BQpairL C \cup BQpairR C = BQ) -> irrationalp (BQpairR C).
proof: Proof. move => hab hc. split; first exact: (BQpair_real hab). move:hab => [ha hb]. move => x /setC_P [xq xtt]. move: xq; rewrite - {1} hc => /setU2_P; case => // /Zo_P[xq [n na nb]]. exists (P (Vg C n)) => //. have yq: ratp (P (Vg C n)) by BQo_tac. move: (ha) => [pa pb pc pd pe]. have hd: inc (P (Vg C n)) (BQpairL C). apply: Zo_i => //;exists (csucc n); fprops. move /(BQpair_aux2a_equiv2 ha): hb => di. apply/setC_P;split => // he; empty_tac1 (P (Vg C n)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)