proposition: Lemma BZ_nz_quo_gcd a b: intp a -> intp b -> a <> \0z -> a %/z (BZgcd a b) <> \0z.
proof: Proof. by move => az bz anz qz; move: (proj1 (BZgcd_div az bz)); rewrite qz BZprod_0r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)