proposition: Lemma BZprod_eq2r x y z: intp x -> intp y -> intp z -> z <> \0z -> x *z z = y *z z -> x = y.
proof: Proof. move => xz yz zz znz eq; apply: (BZdiff_diag_rw xz yz); ex_middle bad. case: (BZprod_nz (ZS_diff xz yz) zz bad znz). by move:(BZprodBl zz xz yz); rewrite eq (BZdiff_diag (ZSp yz zz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)