proposition: Lemma BQpair_rational2 x: ratp x -> exists C, [/\ BQpairR C = BR_of_Q x, BQpair C & BQpair_aux3 C].
proof: Proof. move => xq. pose k n := BQ_of_Zinv (BZ_of_nat (csucc n)). have Hb: forall n, natp n -> k n = BQinv (BQ_of_nat (csucc n)). by move => n nN; rewrite /k - (BQinv_Z ( BQpsS_fromN1 nN)). have Hc: forall n, natp n -> inc (k n) BQps. by move => n nN; rewrite (Hb _ nN); apply: QpsS_inv; apply: BQpsS_fromN. have He: forall n, inc n Nat -> k (csucc n) <q k n. move => n nN; rewrite (Hb _ nN) (Hb _ (NS_succ nN)). apply /(BQinv_mon2 (BQpsS_fromN (NS_succ nN)) (BQpsS_fromN nN)). apply/ qlt_cN; fprops. set C := Lg Nat (fun n => J (x -q k n) (x +q k n)). have Hf: BQpair_aux C. rewrite /C;split. + fprops. + by aw. + hnf; aw; move => n nN; rewrite LgV//; move: (BQps_sBQ (Hc _ nN)) => h. by apply:setXp_i; [apply:QS_diff | apply:QSs ]. + hnf; aw => n nN;move:(NS_succ nN) => nsN; rewrite !LgV//; aw. move:(He _ nN) => / qlt_opp lt1. by move /(BQsum_lt2l (proj31_1 lt1)(proj32_1 lt1) xq): (lt1). + hnf; aw => n nN;move:(NS_succ nN) => nsN; rewrite !LgV//; aw. move:(He _ nN) => lt1. by move /(BQsum_lt2l (proj31_1 lt1)(proj32_1 lt1) xq): (lt1). have Hd:BQpair_aux2b C. apply/(BQpair_aux2a_equiv Hf); rewrite /C; move => n nN; rewrite !LgV//; aw. move / qlt0xP: (Hc _ nN) => l1. move / qgt0xP: (BQopp_positive1 (Hc _ nN)) => l2. move: (qlt_ltT l2 l1) => lt1. by move /(BQsum_lt2l (proj31_1 lt1)(proj32_1 lt1) xq): lt1. have Hg: inc x (BQ -s (BQpairL C \cup BQpairR C)). apply/setC_P; split => // /setU2_P; case => /Zo_P [_ [n nN]]. rewrite /C LgV//; aw => sa. move:(BQsum_Mps xq (Hc _ nN)) => se. move: (Hc _ nN) => sb; move:(BQps_sBQ sb) => sc. move/(BQsum_lt2l xq (proj32_1 sa) sc): sa. rewrite (BQsum_diff sc xq) BQsumC; move => [sf _]; BQo_tac. rewrite /C LgV//; aw;move:(BQsum_Mps xq (Hc _ nN)) => sa [sb _]; BQo_tac. have Hh: forall t, x <q t -> inc t (BQpairR C). move => z lxz; move:(proj32_1 lxz) => zq; apply/Zo_P; split => //. move/(qlt_diffP1 xq zq): lxz => / qlt0xP /QpsS_inv => h. move: (BQ_floorp4 (BQps_sBQ h)) => [n nN na]. have nb:BQ_of_nat n <q BQ_of_nat (csucc n) by apply/ qlt_cN; fprops. move:(qlt_ltT na nb) => /(BQinv_mon2 (BQpsS_fromN nN) h). rewrite (BQinv_K (QS_diff zq xq)) => sa. move/(qlt_diffP3 (proj31_1 sa) zq xq): sa; rewrite BQsumC => sb. by exists n => //; rewrite /C LgV//; aw; rewrite Hb. have Hi: BQpairR C = BR_of_Q x. set_extens t; last by move => /Zo_P [tq tx]; apply: Hh. move/Zo_P => [tq [n na nb]]; apply/Zo_P; split => //. move: nb; rewrite /C LgV//;aw. move:(BQsum_Mps xq (Hc _ na)) => sa sb; BQo_tac. exists C; split => //. exists x; apply: set1_pr => // z /setC_P [zq h]. case: (qleT_ell xq zq) => // lzq; case: h; apply/setU2_P; [right | left ]. by apply:Hh. apply/Zo_P; split => //. move/(qlt_diffP1 zq xq): lzq => / qlt0xP /QpsS_inv => h. move: (BQ_floorp4 (BQps_sBQ h)) => [n nN na]. have nb:BQ_of_nat n <q BQ_of_nat (csucc n) by apply/ qlt_cN; fprops. move:(qlt_ltT na nb) => /(BQinv_mon2 (BQpsS_fromN nN) h). rewrite (BQinv_K (QS_diff xq zq)) => ha. move: (proj31_1 ha) => hb. move/(qlt_diffP3 hb xq zq): ha; rewrite BQsumC => hc. move/(qlt_diffP3 zq xq hb): hc => hd. by exists n =>//; rewrite /C LgV//; aw; rewrite Hb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)