proposition: Lemma BQ_of_Z_iQms z: inc z BZms -> inc (BQ_of_Z z) BQms.
proof: Proof. move => zn. by apply: Zo_i; [ apply:(BQ_of_Z_iQ (BZms_sBZ zn)) | rewrite /BQ_of_Z; aw]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)