proposition: Lemma BZprod_ACA a b c d: intp a -> intp b -> intp c -> intp d -> (a *z b) *z (c *z d) = (a *z c) *z (b *z d).
proof: Proof. move => az bz cz dz; move: (ZSp cz dz) (ZSp bz dz)=> cdz bdz. by rewrite -!BZprodA // (BZprod_CA bz cz dz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)