proposition: Lemma rati_lt1 a b (A := BQ_of_Z a) (B := BQ_of_Z b): inc a BZp -> inc b BZps -> rat_iterator (A /q (A +q B)) = (A +q B) /q B.
proof: Proof. move => azp bzps. have az: intp a by apply:BZp_sBZ. have bz: intp b by apply:BZps_sBZ. move:(BQ_of_Z_iQ az)(BQ_of_Z_iQ bz)(BQ_of_Z_iQp azp)(BQ_of_Z_iQps bzps). rewrite -/A -/B => aq bq aqp bqps. have ha: A <q A +q B by apply:(BQsum_Mps aq bqps). have:inc (A +q B) BQps by apply/ qlt0xP; apply: qle_ltT ha; apply/ qle0xP. move/BQps_iP => [/BQp_sBQ abq abnz]. rewrite /rat_iterator (BQ_floor_zero aqp ha) /BQdouble (BQprod_0r QS2). rewrite (BQsum_0r QS1) (BQdiff_div QS1 aq abq abnz). by rewrite (BQprod_1l abq) (BQdiff_sum aq bq) (BQinv_div bq abq). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)