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.