proposition: Lemma BQ_floorp4 x: ratp x -> exists2 y, inc y Nat & x <q (BQ_of_nat y).
proof: Proof. move /BQ_floorp3 => [m mz le1]. case/BZ_i0P: (mz) => h. move/zgt0xP: h => [/(qle_cZ mz ZS0)] => ha. exists \0c;[ apply:NS0 | BQo_tac]. exists (BZ_val m); first by apply: BZ_valN. by rewrite/BQ_of_nat (BZp_hi_pr h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)