# Library Coq.Numbers.NatInt.NZMul

Require Import NZAxioms NZBase NZAdd.
Module Type NZMulPropSig
(Import NZ : NZAxiomsSig')(Import NZBase : NZBasePropSig NZ).
Include NZAddPropSig NZ NZBase.
Theorem mul_0_r : forall n, n * 0 == 0.
Theorem mul_succ_r : forall n m, n * ( S m ) == n * m + n.
Hint Rewrite mul_0_r mul_succ_r : nz.
Theorem mul_comm : forall n m, n * m == m * n.
Theorem mul_add_distr_r : forall n m p, ( n + m ) * p == n * p + m * p.
Theorem mul_add_distr_l : forall n m p, n * ( m + p ) == n * m + n * p.
Theorem mul_assoc : forall n m p, n * ( m * p ) == ( n * m ) * p.
Theorem mul_1_l : forall n, 1 * n == n.
Theorem mul_1_r : forall n, n * 1 == n.
End NZMulPropSig.