proposition: Lemma BQfloor_pos x (m := BQfloor x): inc x BQp -> ( BQ_of_Z m = BQ_of_nat (P m) /\ natp (P m)).
proof: Proof. move => xp; move: (QpS_floor xp) => mzp. split; first by rewrite /BQ_of_nat (BZp_hi_pr mzp). exact: (BZ_valN (BZp_sBZ mzp)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)