proposition: Lemma BQpair_irrational3 x: irrationalp x -> exists C, [/\ BQpairR C = x, BQpair C & BQpairL C \cup BQpairR C = BQ].
proof: Proof. move => [[pa pb pc pd pe] pf]. pose PR p q := [/\ (P p) <q P q, Q q <q Q p & (Q q -q P q) <q BQhalf (Q p -q P p)]. set E := (BQ -s x) \times x. have Ha: forall p, inc p E -> exists q, inc q E /\ PR p q. move => p /setX_P [qa qb qd]; move:(pf _ qb) => Hi. move/setC_P: qb => [qb qc]. case: (qleT_ell (pa _ qd) qb) => lt1. by case:qc; rewrite - lt1. case: qc; apply:(pd _ _ qd lt1). move:(BQmiddle_comp lt1); set a := BQmiddle (P p) (Q p). move => [lt2 lt3]. have aq: ratp a by BQo_tac. case: (inc_or_not a x) => iax. move:Hi => [b ba bb]; exists (J b a); split;first by apply:setXp_i. hnf; saw. move/ (BQsum_lt2r (proj31_1 bb) (proj32_1 bb) (QSo aq)): (bb). move => / qlt_opp;rewrite (BQoppB (proj32_1 bb) (proj32_1 lt2)). rewrite (BQoppB qb (proj32_1 lt2)). by rewrite - (BQ_middle_prop2 qb (proj32_1 lt1)). move: (pe _ qd) => [b bx lt4]; exists (J a b). split;first by apply:setXp_i; [ by apply/setC_P | done]. move/ (BQsum_lt2r (proj31_1 lt4) (proj32_1 lt4) (QSo aq)): (lt4) => lt5. by hnf; saw; rewrite - (BQ_middle_prop1 qb (proj32_1 lt1)). pose np p:= choose (fun q => inc q E /\ PR p q). have npp: forall p, inc p E -> (inc (np p) E /\ PR p (np p)). move => p pE; apply:(choose_pr (Ha _ pE)). move:(setC_ne (conj pa pc)) => [a0 a0x]. move:pb =>[b0 b0x]. have qbE: inc (J a0 b0) E by apply:setXp_i. move: (induction_defined_pr np (J a0 b0)). set f := induction_defined np (J a0 b0). move => [fa fb fc fd]. pose F := Lg Nat (Vf f). have Hb: forall n, natp n -> Vg F n = Vf f n. rewrite /F => n nN; rewrite !LgV //. have Hc1: Vg F \0c = J a0 b0 by rewrite (Hb _ NS0) fc. have Hc2: forall n, natp n -> Vg F (csucc n) = np (Vg F n). by move => n nN; rewrite (Hb _ nN) - (fd _ nN) (Hb _ (NS_succ nN)). have Hd: forall n, natp n -> inc (Vg F n) E /\ PR (Vg F n) (Vg F (csucc n)). apply:Nat_induction. rewrite (Hc2 _ NS0) Hc1; split => //; exact (proj2 (npp _ qbE)). move => n nN [ha hb]; move:(NS_succ nN) => hc. rewrite (Hc2 _ hc)(Hc2 _ nN); move:(proj1 (npp _ ha)) => sa. split; [exact | exact:(proj2 (npp _ sa))]. have He:forall n, natp n -> inc (Vg F n) (BQ \times BQ). by move => n /Hd [/setX_P [qa /setC_P [qb _] /pa qc] _]; apply/setX_P. have Hf1:forall n, natp n -> P (Vg F n) <q P (Vg F (csucc n)). by move => n /Hd [_ []]. have Hf2:forall n, natp n -> Q (Vg F (csucc n)) <q Q (Vg F n). by move => n /Hd [_ []]. have Hg: BQpair_aux F by split => //;rewrite/F; fprops; aw. have Hg': BQpair_aux2b F. apply/(BQpair_aux2a_equiv Hg) => n nN. move:(proj1 (Hd _ nN)) => /setX_P [qa /setC_P [qb qc] qd]. case:(qleT_ell qb (pa _ qd)) => // ha; case: qc; first by ue. apply: (pd _ _ qd ha). pose delta n := (Q (Vg F n) -q P (Vg F n)). have deltap: forall n, natp n -> inc (delta n) BQps. move => n nN; move: (proj1 (Hd _ nN)) => /setX_P [_ /setC_P [sa sb] sc]. apply/ qlt0xP; apply/ (qlt_diffP1 sa (pa _ sc)). case:(qleT_ell sa (pa _ sc))=> // ha; case: sb;first by rewrite ha. apply: (pd _ _ sc ha). have Hh: forall n, natp n -> delta n <=q (b0 -q a0) /q (BQ_of_nat (\2c ^c n)). move/setC_P: a0x => [aq _]; move:(QS_diff (pa _ b0x) aq) => h. rewrite/delta;apply: Nat_induction. rewrite Hc1; aw; rewrite cpowx0 /BQ_of_nat -/BZ_one -/BQ_one. rewrite (BQdiv_x1 h); apply: (qleR h). move => n nN; rewrite (cpow_succ _ nN); set s := _ /q _ => Hrec. have ha: ratp (BQ_of_nat (\2c ^c n)) by apply: QS_of_nat; fprops. have hb: ratp (BQ_of_nat \2c) by apply: (QS_of_nat NS2). rewrite (BQprod_cN (NS_pow NS2 nN) NS2) (BQdiv_div2 h ha hb). rewrite -/s /BQ_of_nat -/BZ_two -/BQ_two -BQhalf_prop. move:(proj2 (Hd _ nN)) => [_ _ hd]. exact (proj1 (qlt_leT hd(BQhalf_mon Hrec))). have Hi: forall d, inc d BQps -> exists2 n, natp n & (delta n <q d). move:(deltap _ NS0); rewrite /delta Hc1; aw => lb. move => d dp; move:(QpsS_div lb dp) => hb. move:(BQ_floorp4 (BQps_sBQ hb)) => [n nN na]. have ha: BQ_of_nat n <q BQ_of_nat (\2c ^c n). apply/ qlt_cN; fprops; apply:(cantor (CS_nat nN)). move:(qlt_ltT na ha) => nb. have hc: inc (BQ_of_nat (\2c ^c n)) BQps. move/ qlt0xP:hb => sa; apply/ qlt0xP; BQo_tac. move/(BQdiv_lt1P (BQps_sBQ lb) hc dp): nb => hd. move:(qlt_ltT (BQhalf_pos1 (deltap _ nN)) (qle_ltT (Hh _ nN) hd)) => he. exists (csucc n); first apply: (NS_succ nN). move: (proj2 (Hd _ nN)) => [_ _ hf]; BQo_tac. have Hj: BQpairR F = x. set_extens t. move /Zo_P => [tq [n nN na]]; move: (proj1 (Hd _ nN)) => /setX_P[_ _ h]. apply: (pd _ _ h na). move => tx; move:(pe _ tx) => [u ux lut]; move:(pa _ tx) (pa _ ux)=> tq uq. have dp: inc (t -q u) BQps. by apply/ qlt0xP; apply/ (qlt_diffP1 uq tq). move:(Hi _ dp) => [n nN ds]; apply:Zo_i => //; exists n => //. move: (proj1 (Hd _ nN)) => /setX_P[ _ /setC_P[sa sb] sc]. have sd: (P (Vg F n)) <q u. case: (qleT_ell sa uq) => // sd; case: sb; [ ue | apply: (pd _ _ ux sd)]. move:(BQsum_Mltlt sd ds); rewrite /delta. by rewrite (BQsum_diff sa (pa _ sc)) (BQsum_diff uq tq). exists F; split => //. set_extens t; first by case /setU2_P => /Zo_P []. move => tq; case: (inc_or_not t x) => tx. by apply/setU2_P; right; rewrite Hj. apply/setU2_P; left. have /pf [y /setC_P[yq yb] yc ]: inc t (BQ -s x) by apply /setC_P. have dp: inc (y -q t) BQps. by apply/ qlt0xP; apply/ (qlt_diffP1 tq yq). move:(Hi _ dp) => [n nN ds]; apply:Zo_i => //; exists n => //. move: (He _ nN) => /setX_P [_ aq bq]. move:(qlt_opp ds);rewrite /delta (BQoppB yq tq) (BQoppB bq aq) => sd. move: (proj1 (Hd _ nN)) => /setX_P[ _ /setC_P[sa sb] sc]. have se: y <q (Q (Vg F n)). case: (qleT_ell yq bq) => // se;case: yb; [ ue |apply: (pd _ _ sc se) ]. by move:(BQsum_Mltlt se sd);rewrite (BQsum_diff yq tq)(BQsum_diff bq aq). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)