proposition: Lemma QS_rati x: ratp x -> inc (rat_iterator x) BQ.
proof: Proof. move => h. apply: QS_inv; apply: (QS_diff _ h); apply: (QSs QS1); apply:QSdouble. by apply: BQ_of_Z_iQ; apply: ZS_floor. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)