proposition: Lemma rati_0: rat_iterator \0q = \1q.
proof: Proof. rewrite /rat_iterator BQfloor_0 / BQdouble (BQprod_0r QS2) (BQsum_0r QS1). by rewrite (BQdiff_0r QS1) BQinv_1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)