proposition: Lemma BQ_of_Zi_pr0 z:intp z -> BQ_of_Zinv z = BQ_of_pair \1z z.
proof: Proof. move => zz. by rewrite /BQ_of_pair -lock /BQ_of_pair_internal BZgcd_C (BZ_coprime1r zz) (BZquo_one zz) (BZquo_one ZS1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)