proposition: Lemma BQfloor_pos2 x (y := BQ_of_nat (P (BQfloor x))): inc x BQp -> y <=q x /\ x <q y +q \1q.
proof: Proof. move => xp; move:(BQfloor_pos xp) => [sa sb]. by move:(BQ_floorp (BQp_sBQ xp)); rewrite sa. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)