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