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