proposition: Lemma BRsqrt2_prop: inc BRsqrt2 BRps /\ BRsquare BRsqrt2 = \2r.
proof: Proof. move: (proj1 sqrt2_irrational) => /BR_P xr. have sp: inc BRsqrt2 BRps. have ha: ~ inc \1q BRsqrt2. move /Zo_hi; rewrite (BQprod_1r QS1); move: qlt_12 => ha [hb _]; BQo_tac. have hb:=(BR_le_aux3 xr QS1 ha). have hc: \0r <r \1r by apply/ rlt0xP; apply:RpsS1. apply/rlt0xP;BRo_tac. split => //; rewrite /BRsquare (BR_prod_aux1 sp sp);set_extens t. move:(BQps_sBQp QpsS2) => hw. move/BR_prod_auxP => [a /Zo_P[ap ha] [b /Zo_P[bp hb] ->]]; apply/Zo_P. have abp:= (QpsS_prod ap bp). split ; [ exact:BQps_sBQ | case:(qleT_el (BQps_sBQ abp)QS2) => // h]. move:(BQprod_Mlelege0 hw (BQps_sBQp abp) h h) => h1. move: (BQps_sBQ ap)(BQps_sBQ bp) => aq bq. move:(BQprod_Mltltge0 hw hw ha hb);rewrite BQprod_ACA // => h2; BQo_tac. move => /Zo_P [ta tb]; apply /BR_prod_auxP. move/BQ_P:(ta) => [_ ha hb _]. move: (BQdiv_numden ta) (BQ_of_Z_iQps hb) (BQ_of_Z_iQ ha). set a := BQ_of_Z (P t); set b := BQ_of_Z (Q t) => pa bp aq. rewrite -pa in tb |- *. move/BQps_iP: (bp) => [/BQp_sBQ bq bnz]. move:(BQprod_Mltgt0 bp tb); rewrite (BQprodC (a /q b)) (BQprod_div bq aq bnz). move => ga2b. have a2q:= QSp QS2 aq. have hc := BZps_sBZ hb. have ap: inc a BQps. move:(QpsS_prod QpsS2 bp) => / qlt0xP h1; apply/ qlt0xP; BQo_tac. set d := \2q *q a +q \1q. set dd:= (\2q *q a) *q (\2q *q a). have deq: BQsquare d = (dd +q \1q) +q \4q *q a. rewrite (BQsum_square a2q QS1) /BQsquare (BQprod_1r a2q) (BQprod_1r QS1). by rewrite -/dd /BQdouble (BQprodA QS2 QS2 aq) BQprod_22. have lt1: \2q *q a *q d +q \1q <q BQsquare d. have ddq: ratp dd by apply:QSp. rewrite deq /d (BQprodDr a2q a2q QS1) -/dd (BQprod_1r a2q). rewrite - (BQsumA ddq a2q QS1) (BQsumC _ \1q) (BQsumA ddq QS1 a2q). have sa:=(BQprod_Mltgt0 ap qlt_24). by apply/(BQsum_lt2l (proj31_1 sa) (proj32_1 sa) (QSs ddq QS1)). have lt2: \1q <=q (a -q \2q *q b) *q b. have te :=(ZSp ZS2 hc). have tc:= ZSo te. have td:intp (P t +z BZopp (\2z *z Q t)) by apply:ZSs. rewrite (BQprod_cZ ZS2 hc) /BQdiff BQopp_cZ. rewrite (BQsum_cZ ha tc); rewrite (BQprod_cZ td hc). apply/ (qle_cZ ZS1 (ZSp td hc)); apply:BZ1_small. apply:ZpsS_prod => //; apply/zlt_diffP => //. move: (ga2b);rewrite (BQprod_cZ ZS2 hc). by move/(qlt_cZ (ZSp ZS2 hc) ha) => hd. have lt3: \2q *q BQsquare (b *q d) <q (a *q b) *q BQsquare d -q ((\2q *q a) *q d +q \1q). have dq: ratp d by exact:(QSs a2q QS1). have d2pq:= (BQpS_square dq); have d2q := (BQp_sBQ d2pq). have a2bq:=QS_diff aq (QSp QS2 bq). have bddq := QSp bq d2q. move:(BQprod_Mlege0 d2pq lt2); rewrite (BQprod_1l d2q) => lt3. move:(qlt_leT lt1 lt3); rewrite - (BQprodA a2bq bq d2q). rewrite (BQprodBl bddq aq (QSp QS2 bq)) (BQprodA aq bq d2q). rewrite - (BQprodA QS2 bq bddq) (BQprodA bq bq d2q). rewrite {2}/BQsquare (BQprod_ACA bq bq dq dq) -/(BQsquare _) => l2. have uq:= (QSs (QSp (QSp QS2 aq) dq) QS1). have vq := QSp (QSp aq bq) d2q. have wq := QSp QS2 (BQp_sBQ (BQpS_square (QSp bq dq))). move/(BQsum_lt2l uq (proj32_1 l2) wq): l2; rewrite (BQsum_diff wq vq) => l3. move: (proj2 (BQsum_lt2r (proj31_1 l3) vq (QSo uq)) l3). by move:(BQdiff_sum uq wq); rewrite BQsumC /BQdiff => hh; rewrite {1} hh. have dp: inc d BQps by exact: (QpsS_sum_rl (QpsS_prod QpsS2 ap) QpsS1). have lt5: \1q <=q (a *q b) *q (d *q d). have ra:= (BQps_sBQp(QpsS_prod QpsS2 ap)). have aap: inc (P t) BZps. move/BZ_i2P: ha; case =>// /BQ_of_Z_iQm hf; case:(BQ_di_pos_neg ap hf). have d2: \1q <=q (a *q b). rewrite (BQprod_cZ ha hc); apply/ (qle_cZ ZS1 (ZSp ha hc)). by apply:BZ1_small; apply:ZpsS_prod. have d1: \1q <=q d by rewrite /d BQsumC; apply: (BQsum_Mp QS1). apply:( BQprod_Mpp1 d2 (BQprod_Mpp1 d1 d1)). have lt4: \0q <q (a *q b) *q (d *q d). apply / qlt0xP; exact: (QpsS_prod (QpsS_prod ap bp) (QpsS_prod dp dp)). pose prop m := (a *q b) *q BQsquare d <q BQsquare (BQ_of_nat m). move:(BQ_floorp4 (proj32_1 lt4)) => [n0 n0N n0a]. have prop3: prop n0. rewrite /prop;move:(BQ_nat_square_monotone n0N) => he; BQo_tac. case: (least_int_prop2 n0N prop3). rewrite /prop /BQsquare (BQprod_0r QS0); move => [hhh _]; BQo_tac. set m := cpred _;move => [mN ma npm]. case: (equal_or_not m \0c) => mz. move: ma; rewrite /prop mz succ_zero /BQsquare (BQprod_1r QS1) => hf; BQo_tac. set c := (BQ_of_nat m). have cp:inc c BQps. apply :BQ_of_Z_iQps; apply/BZps_iP; split; first by apply:BZ_of_natp_i. by move/BZ_of_nat_inj. move: (BQps_sBQ cp) (BQps_sBQ dp) => cq dq. case: (qleT_el (QSp cq cq) (proj31_1 ma)) => // hf. have lt6: c /q (b *q d) <=q (a*q d) /q c. apply/ (BQdiv_Mlelege0 cq (QpsS_prod bp dp) (QSp aq dq) cp). by rewrite (BQprod_ACA bq dq aq dq) (BQprodC b). case: (qleT_el cq (QSp aq dq)) => lt7; last first. move:(BQprod_Mltltgt0 cp (QpsS_prod ap dp) lt7 lt7). rewrite (BQprod_ACA aq dq aq dq) => lt8. move: (qlt_leT lt8 hf). move/(BQprod_plt2r (QSp aq aq) (QSp aq bq) (QpsS_prod dp dp)). rewrite (BQprodC _ b); move/(BQprod_plt2r aq bq ap) => lab. suff H: b <=q \2q *q b by case:(qleNgt (qleT (proj1 lab) H) ga2b). rewrite BQprodC; apply:(BQprod_Mpp (BQps_sBQp bp) (proj1 qlt_12)). have lt8: (\1q +q \2q *q c) <=q ((\2q *q a) *q d +q \1q). move: (BQprod_Mlege0 (BQps_sBQp QpsS2) lt7). rewrite BQprodC (BQprodC _ \2q) (BQprodA QS2 aq dq) (BQsumC _ \1q)=> h. exact:(proj2 (BQsum_le2l (proj31 h)(proj32 h) QS1) h). move: ma; rewrite /prop /BQ_of_nat (Nsucc_rw mN) - (BZsum_cN mN NS1). rewrite - (BQsum_cZ (BZ_of_nat_i mN) ZS1) -/(BQ_of_nat _) -/c -/BQ_one. rewrite (BQsum_square cq QS1) /BQsquare (BQprod_1r cq) (BQprod_1r QS1). rewrite - (BQsumA (QSp cq cq) QS1 (QSp QS2 cq)) => lt9. move/(qle_oppP (proj31 lt8)(proj32 lt8)): lt8 => le88. move:(BQsum_Mltle lt9 le88). set X := ( X in _ <q X ). have ->: X = c *q c. by rewrite /X -/(_ -q _) (BQdiff_sum1 (QSs QS1 (QSp QS2 cq)) (QSp cq cq)). move => lt10; move: (qlt_leT lt3 (proj1 lt10)) => lt11. set u := c /q (b *q d). move: (QpsS_prod bp dp) => sa;move: (QpsS_prod sa sa) => sb. have u2: inc u BRsqrt2. apply/Zo_P; split; first apply:(QpsS_div cp sa). move/ (BQprod_Mltgt0 (QpsS_inv sb)): lt11. move/BQps_iP: (sb) => [ /BQp_sBQ sc qdnz]. rewrite (BQprodC \2q) -/(_ /q _) (BQdiv_prod sc QS2 qdnz). have -> //:(c *q c) *q BQinv ((b *q d) *q (b *q d)) = u *q u. move: (QSp bq dq) => se; move:(QS_inv se) => sf. by rewrite (BQprod_inv se se) (BQprod_ACA cq cq sf sf). set v := (a *q d) /q c. have v2 : inc v BRsqrt2. case: (equal_or_not u v) => cuv; first by rewrite - cuv; exact u2. move: (sqrt2_irrational) => [[_ _ _ h _] _]; exact:(h _ _ u2 (conj lt6 cuv)). exists u; [exact | exists v; [ exact |]]. have sf:=(QS_div aq bq). move/BQps_iP: (dp) => [_ dnz]. move/BQps_iP: (cp) => [_ cnz]. rewrite /u/v /BQdiv (BQprodC _ (BQinv c)). rewrite (BQprod_ACA cq (QS_inv (QSp bq dq)) (QS_inv cq)(QSp aq dq)). rewrite (BQprodC (BQinv (b *q d))) (BQprod_inv bq dq). rewrite (BQprod_ACA aq dq (QS_inv bq) (QS_inv dq)). rewrite (BQprod_inv1 dq dnz). by rewrite (BQprod_1r sf) (BQprod_inv1 cq cnz) (BQprod_1l sf). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)