proposition: Lemma QpsS_of_nat n: natp n -> n <> \0c -> inc (BQ_of_nat n) BQps.
proof: Proof. move => sa sn; apply:BQ_of_Z_iQps; apply/BZps_iP. split; [by apply:BZ_of_natp_i | by move/pr1_def]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)