proposition: Lemma BZprodDl n m p: intp n -> intp m -> intp p -> ( m +z p) *z n = (m *z n) +z (p *z n).
proof: Proof. by move => pa pb pc; rewrite (BZprodC) (BZprodC m) (BZprodC p);apply:BZprodDr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)