proposition: Lemma BQ_floorp3 x: ratp x -> exists2 y, inc y BZ & x <q (BQ_of_Z y).
proof: Proof. move => xq; move: (ZS_floor xq) => yz; move: (BQ_floorp xq) => [_]. rewrite (BQsum_cZ yz ZS1) => h. exists (BQfloor x +z \1z) => //; apply:(ZSs yz ZS1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)