proposition: Lemma BZprod_eq2l x y z: intp x -> intp y -> intp z -> z <> \0z -> z *z x = z *z y -> x = y.
proof: Proof. by move => xz yz zz znz; rewrite BZprodC (BZprodC z); apply: BZprod_eq2r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)