proposition: Lemma rati_1: rat_iterator \1q = \2hq.
proof: Proof. rewrite /rat_iterator (BQfloor_Z ZS1) /BQdouble (BQprod_1r QS2). by rewrite (BQdiff_sum QS1 QS2) BQinv_2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)