proposition: Lemma BZprod_CA x y z: intp x -> intp y -> intp z -> x *z (y *z z) = y *z (x *z z).
proof: Proof. by move => xz yz zz;rewrite (BZprodA xz yz zz) (BZprodA yz xz zz) (BZprodC x y). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)