proposition: Lemma BQ_floorp x (y := (BQ_of_Z (BQfloor x))) : ratp x -> (y <=q x /\ x <q y +q \1q).
proof: Proof. move => xq; move: (xq) => /BQ_P [_ pa pb _]. move/ BZps_iP: (pb) => [/ BZp_sBZ bz bnz]. move: (BZdvd_correct pa bz bnz); rewrite -/(BQfloor x). set r := (P x %%z Q x); move => [sa sb [sc sd _]]. rewrite (BZabs_pos (BZps_sBZp pb)) in sd. have re: intp r by apply: ZS_rem. have sf: intp (Q x *z BQfloor x) by apply: ZSp. have yQ: ratp y by apply:BQ_of_Z_iQ; apply: ZS_floor. have rbb: inc (BQ_of_Z (Q x)) BQps by by apply: BQ_of_Z_iQps. have ra: ratp (BQ_of_Z r) by apply: BQ_of_Z_iQ. have rb: ratp (BQ_of_Z (Q x)) by apply: BQ_of_Z_iQ. have rc: BQ_of_Z (Q x) <> \0q by move/pr1_def. move: (BQsum_div yQ ra rb rc). rewrite {2} /y BQprodC (BQprod_cZ bz sa) (BQsum_cZ sf re) - sc. rewrite (BQdiv_numden xq) => <-; split. by apply:BQsum_Mp=> //;apply: QpS_div; apply:BQ_of_Z_iQp =>//;apply:BZps_sBZp. have rd: ratp (BQ_of_Z r /q BQ_of_Z (Q x)) by apply: QS_div. apply / (BQsum_lt2l rd QS1 yQ); apply /(BQprod_Mlt1 ra rbb). apply/ qlt_cZ => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)