proposition: Lemma rati_pos x: inc x BQp -> inc (rat_iterator x) BQps.
proof: Proof. move =>h; apply:QpsS_inv. move:(QpS_floor h) (BQp_sBQ h) => fp xq. move: (BQ_of_Z_iQp fp) (proj2 (BQ_floorp xq)). set y := BQ_of_Z _ => yp lt1. have yq: ratp y by exact: (BQp_sBQ yp). rewrite - (BQdouble_p yq) (BQsumA QS1 yq yq) (BQsumC (\1q +q y)). rewrite /BQdiff - (BQsumA yq (QSs QS1 yq) (QSo xq)). by apply: (QpsS_sum_r yp); apply /(qlt_diffP xq (QSs QS1 yq)); rewrite BQsumC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)