proposition: Lemma BZgcd_nz1 a b: intp a -> intp b -> (a <> \0z \/ b <> \0z) -> BZgcd a b <> \0z.
proof: Proof. by move => az bz h gnz; move: (BZgcd_nz az bz gnz) => [a0 b0]; case: h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)