proposition: Lemma rati_gt1 a b (c := (a +z b) -z \2z *z (a %%z b)) (A := BQ_of_Z a) (B := BQ_of_Z b) (C := BQ_of_Z c): inc a BZp -> inc b BZps -> (inc c BZps /\ rat_iterator ((A +q B) /q B) = B /q (B +q C)).
proof: Proof. rewrite /rat_iterator. move => azp bzps; move:(BZp_sBZ azp) => az. move/BZps_iP: (bzps) => [ bzp bnz]; move: (BZp_sBZ bzp) => bz. move:(BZdvd_correct az bz bnz). set q := (a %/z b); set r := (a %%z b); move => [qz rzp [eq1]]. rewrite (BZabs_pos bzp) => lt1 /BZp_sBZ rz. have eq2: (a +z b) = (q +z \1z) *z b +z r. rewrite eq1 BZsumC (BZsumA bz (ZSp bz qz) rz) (BZprodDl bz qz ZS1). by rewrite (BZprod_1l bz) (BZsumC b) BZprodC. move:(BQ_of_Z_iQ az)(BQ_of_Z_iQ bz); rewrite -/A -/B => aq bq. move:(BQ_of_Z_iQp azp)(BQ_of_Z_iQps bzps); rewrite -/A -/B => aqp bqps. have fq: ratp ((A +q B) /q B) by apply:QS_div => //; apply:QSs. have q1z := (ZSs qz ZS1); have q1q:=(BQ_of_Z_iQ q1z). have eq0: c = (a -z r) +z (b -z r). rewrite /c -/r (BZdoublep rz). by rewrite(BZsum_ACA az (ZSo rz) bz (ZSo rz))- (BZoppD rz rz). have czp: inc c BZps. rewrite eq0; apply:ZpsS_sum_r; last by apply/zlt0xP; apply/(zlt_diffP1 rz bz). rewrite eq1 (BZdiff_sum1 rz (ZSp bz qz)). exact: (ZpS_prod bzp(ZpS_quo azp bzp)). have cz:= (BZps_sBZ czp); have abz:= (ZSs az bz). have le1: BQ_of_Z (q +z \1z) <=q (A +q B) /q B. apply /(Qdiv_Mlelege1 q1q (QSs aq bq) bqps). have ha:= (ZSp q1z bz). rewrite (BQsum_cZ az bz) (BQprod_cZ q1z bz). apply /(qle_cZ ha abz). rewrite eq2;apply:(BZsum_Mp ha rzp). have le2: (A +q B) /q B <q BQ_of_Z (q +z \1z) +q \1q. apply/(Qdiv_Mltltge2 (QSs aq bq) bqps (QSs q1q QS1)). rewrite (BQprodDr bq q1q QS1) (BQprod_1r bq). apply /(BQsum_lt2r aq (QSp bq q1q) bq). rewrite (BQprod_cZ bz q1z); apply/(qlt_cZ az (ZSp bz q1z)). rewrite eq1 (BZprodDr bz qz ZS1) (BZprod_1r bz). by apply/(BZsum_lt2l rz bz (ZSp bz qz)). split; first exact. have ->: (BQfloor ((A +q B) /q B)) = q +z \1z. by symmetry;apply: (BQ_floorp2 fq q1z). have ->: (A +q B) /q B = \1q +q A /q B. by rewrite (BQsum_div QS1 aq bq (BQps_nz bqps)) (BQprod_1l bq) BQsumC. move: (QSdouble q1q) => s1q; move: (QSs QS1 s1q) => sq. have q12z:= (ZSp ZS2 q1z); have q12bz:= (ZSp q12z bz). rewrite (BQdiff_diff2 sq QS1 (QS_div aq bq)) (BQdiff_sum QS1 s1q). rewrite (BQdiff_div s1q aq bq (BQps_nz bqps)). rewrite (BQinv_div (QS_diff (QSp s1q bq) aq) bq). rewrite /BQdouble (BQprod_cZ ZS2 q1z)(BQprod_cZ q12z bz). rewrite (BQdiff_cZ q12bz az) (BQsum_cZ bz cz). congr (B /q (BQ_of_Z _)). apply: (BZsum_eq2r (ZS_diff q12bz az) (ZSs bz cz) az). rewrite BZsumC (BZsum_diff az q12bz) (BZsumC _ a) (BZsumA az bz cz). rewrite (BZsumA abz abz (ZSo (ZSp ZS2 rz))) - (BZdoublep abz). rewrite /BZdiff (BZopp_prod_r ZS2 rz) - (BZprodDr ZS2 abz (ZSo rz)). rewrite - (BZprodA ZS2 q1z bz); congr (\2z *z _). rewrite (BZsum_AC az bz (ZSo rz)) eq1 -/(_ -z _) (BZdiff_sum1 rz (ZSp bz qz)). by rewrite (BZprodDl bz qz ZS1)(BZprod_1l bz) BZprodC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)