proposition: Lemma BQ_of_Zi_iQps z: inc z BZps -> inc (BQ_of_Zinv z) BQps.
proof: Proof. move => zp;apply: Zo_i; last by rewrite /BQ_of_Zinv; aw; apply: ZpsS1. rewrite (BQ_of_Zi_pr0 (BZps_sBZ zp));apply: BQ_of_pair_prop4 => //; apply: ZS1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)