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