proposition: Lemma BZgcd_nz a b: intp a -> intp b -> BZgcd a b = \0z -> (a = \0z /\ b = \0z).
proof: Proof. by move => az bz h; move: (BZgcd_div az bz); rewrite h !BZprod_0l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)