proposition: Lemma BQprod_cZ x y: intp x -> intp y -> BQ_of_Z x *q BQ_of_Z y = BQ_of_Z (x *z y).
proof: Proof. move => xz yz; move: (ZSp xz yz) => xyz. rewrite /BQ_of_Z /BQprod /BQ_of_pair -lock /BQ_of_pair_internal; aw. rewrite (BZprod_1l ZS1) (BZgcd_x1 xyz) ! BZquo_one //; apply:ZS1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)