proposition: Lemma BQpsS_fromN1 n: natp n -> inc (BZ_of_nat (csucc n)) BZps.
proof: Proof. move => nN; apply /BZps_iP; split. by apply:BZ_of_natp_i;apply:NS_succ. move/BZ_of_nat_inj; apply: succ_nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)