proposition: Lemma BZprod_nz x y: intp x -> intp y -> x <> \0z -> y <> \0z -> x *z y <> \0z.
proof: Proof. move => xz yz xnz ynz zz. move: (congr1 P zz); rewrite BZprod_val BZ0_val; apply: cprod2_nz. + move => pz; case: xnz; apply: (BZ_0_if_val0 xz pz). + move => pz; case: ynz; apply: (BZ_0_if_val0 yz pz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)