proposition: Lemma BQ_of_Z_iQps z: inc z BZps -> inc (BQ_of_Z z) BQps.
proof: Proof. move => zp. by apply: Zo_i; [ apply:(BQ_of_Z_iQ (BZps_sBZ zp)) | rewrite /BQ_of_Z; aw]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)