proposition: Lemma BQ_floorp2 x z (y := (BQ_of_Z z)) : ratp x -> intp z -> (y <=q x /\ x <q y +q \1q) -> z = BQfloor x.
proof: Proof. move => xq zz [pa pb]; move:(BQ_floorp xq) => [pc pd]. have pe: inc (BQfloor x) BZ by apply:ZS_floor. have pf: intp (z +z \1z) by apply:(ZSs zz ZS1). have pg:intp (BQfloor x +z \1z) by apply:ZSs ZS1. rewrite (BQ_floor_aux pe) in pd; rewrite (BQ_floor_aux zz) in pb. move /(qlt_cZ pe pf): (qle_ltT pc pb) => /(zlt_succ1P pe zz) l1. move /(qlt_cZ zz pg): (qle_ltT pa pd) => /(zlt_succ1P zz pe) l2. BZo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)