proposition: Lemma sqrt2_irrational: irrationalp BRsqrt2.
proof: Proof. have sw:=BQ_square_2. have sa:= qlt_12. have sc:= QpsS2. split; first split. + by move => t /Zo_S /BQps_sBQ. + exists \2q; apply:Zo_i; first apply: QpsS2. by move:(BQprod_Mltgt0 QpsS2 qlt_12); rewrite (BQprod_1l QS2). + by move => h; move: QS0; rewrite /ratp -h => /Zo_S => /BQps_iP [ _]. + move => x y /Zo_P [pa pb] pc; apply: Zo_i. apply / qlt0xP; move/ qlt0xP: pa => pd; BQo_tac. move:(BQprod_Mltltge0 (BQps_sBQp pa) (BQps_sBQp pa) pc pc) => pd; BQo_tac. + move => x /Zo_P [pa pb]. set y := (x *q x +q \2q) /q (\2q *q x). have ya:=(QpsS_prod sc pa). have xq:= (BQps_sBQ pa). have yb:= (QpsS_sum_rl(QpsS_prod pa pa) sc). have ybb := (BQps_sBQ yb). have yc:= (QSp xq xq). have yd: inc y BQps by apply: QpsS_div. have ye:=(QS_diff yc QS2). have yf:= (BQps_sBQ ya). set z := (x*q x -q \2q) /q (\2q *q x). move: (QpsS_prod ya ya) => /BQps_iP [ _ yg]. have yh : BQsquare y = \2q +q (BQsquare z). rewrite (BQdiv_square ybb yf)(BQdiv_square ye yf). rewrite (BQsum_div QS2 (QSp ye ye) (QSp yf yf) yg). rewrite (BQsumdiff_square (QSp xq xq) QS2). rewrite -BQprod_22 (BQprodA (QSp QS2 QS2) yc QS2). by rewrite (BQprod_ACA QS2 QS2 xq xq) (BQprodC _ \2q). have yi: y <q x. rewrite - (BQdiv_x1 xq). apply /(BQdiv_Mltltge0 ybb ya xq QpsS1); rewrite (BQprod_1r ybb). rewrite - (BQprodA QS2 xq xq) - /(BQdouble _) - (BQdouble_p yc). by apply/(BQsum_lt2l QS2 yc yc). have zp: inc z BQps by apply:QpsS_div => //; apply/ (qlt_diffP QS2 yc). have yj: \2q <q y *q y. rewrite -/(BQsquare _) yh;apply: (BQsum_Mps QS2);apply:(QpsS_prod zp zp). exists y; [ by apply/Zo_P | exact]. + move => x /setC_P [xq xp]; case/BQ_i2P: xq; last first. move => / qge0xP xn; move:(qle_ltT xn qlt_01) => x1; exists \1q => //. apply /setC_P; split; [exact:QS1 | apply/ Zo_P]. rewrite (BQprod_1l QS1); move => [_ [h _]]; BQo_tac. move => xpo; move /Zo_P: (xpo)=> [xq ap]. case: (qleT_ell QS2 (QSp xq xq)). - by move => h; case:(sw _ xq). - by move => h; case: xp; apply/ Zo_P. - rewrite -/(BQsquare _); move: (BQ_squarep xq) => ->. rewrite {1} /BQ_two /BQ_of_Z; move/ qltP => [ _ _]; aw. move /BQ_P: (xq); set a := P x; set b := Q x. move => [_ az bz _]; rewrite (BZprod_1r (ZSp az az)) => eq1. move /(zlt_succ2P (proj31_1 eq1) (proj32_1 eq1)): eq1 => eq2. move:(BQdiv_numden xq); rewrite -/a -/b. set a' := BQ_of_Z a; set b' := BQ_of_Z b => xv. have a'qps:=(BQ_of_Z_iQps ap). have b'qps:=(BQ_of_Z_iQps bz). move /BQps_iP:(a'qps) => [ /BQp_sBQ a'q a'nz]. have b'q:= BQps_sBQ b'qps. set yn := a' +q BQinv (\4q *q a'). set y := BQdiv yn b'. have p4z:= BZprod_22. have ha0 := (QpsS_prod QpsS4 a'qps). have hf:=BQps_sBQ ha0. have ha:= (QpsS_inv ha0). have ha' := BQps_sBQ ha. have ynq: ratp yn by apply:QSs. have yq: ratp y by apply:QS_div. have lt1: x <q y. rewrite /y /yn (BQdiv_sumDl b'q a'q ha') xv; apply: BQsum_Mps => //. by apply:QpsS_div. suff ly2: BQsquare y <=q \2q. exists y => //;apply/setC_P; split => // /Zo_P [_ y2]; BQo_tac. rewrite (BQdiv_square ynq b'q). apply/ (BQdiv_Mle1 (QSp ynq ynq) QS2 (QpsS_prod b'qps b'qps)). move /(qle_cZ (proj31 eq2) (proj32 eq2)): eq2. have bz0 := (BZps_sBZ bz). have bbz:= (ZSp bz0 bz0). rewrite (BQprodC \2q) - (BQprod_cZ bbz ZS2) - (BQprod_cZ bz0 bz0). apply: qleT;rewrite - (BQsum_cZ (ZSp az az) ZS1) -/BQ_one. move: (QSp a'q a'q) (QSp ha' ha') (QSp QS2 (QSp a'q ha')) => hb hc hd. rewrite -(BQprod_cZ az az) -/a' /yn -/(BQsquare _)(BQsum_square a'q ha'). rewrite - (BQsumA hb hc hd); apply/(BQsum_le2l (QSs hc hd) QS1 hb). have he := (BQps_sBQ QpsS4). have hg:= (QS_inv he). have sp4s:=BZps_sBZp ZpsS4. have hi:=(ZSp ZS4 az). have ->: \2q *q (a' *q BQinv (BQ_of_Z \4z *q a')) = \2hq. rewrite (BQprodC _ a') (BQprod_inv a'q he). rewrite (BQprodA a'q (QS_inv a'q) hg)(BQprod_inv1 a'q a'nz)(BQprod_1l hg). rewrite -BQprod_22 (BQprod_inv QS2 QS2). by rewrite (BQprod_div QS2 (QS_inv QS2) BQ2_nz) BQinv_2. rewrite - BQdouble_half2; apply/(BQsum_le2r hc QSh2 QSh2). rewrite - (BQprod_inv hf hf) - (BQdiv_1x (QSp hf hf)) - BQinv_2. rewrite -(BQdiv_1x QS2); apply/(BQinv_mon (QpsS_prod ha0 ha0) QpsS2). rewrite (BQprod_cZ ZS4 az) (BQprod_cZ hi hi). apply/(qle_cZ ZS2 (ZSp hi hi)). have hj: \4z <=z (\4z *z a) by apply:BZprod_Mpp. move:(BZprod_Mlege0 (BZps_sBZp (ZpsS_prod ZpsS4 ap)) (zleT zle_24 hj)). apply: zleT; apply:BZprod_Mpp (BZps_sBZp ZpsS2) (ZpsS_prod ZpsS4 ap). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)