Library Coq.Numbers.NatInt.NZMul



Require Import NZAxioms.
Require Import NZAdd.

Module NZMulPropFunct (Import NZAxiomsMod : NZAxiomsSig).
Module Export NZAddPropMod := NZAddPropFunct NZAxiomsMod.
Open Local Scope NatIntScope.

Theorem NZmul_0_r : forall n : NZ, n * 0 == 0.

Theorem NZmul_succ_r : forall n m : NZ, n * (S m) == n * m + n.

Theorem NZmul_comm : forall n m : NZ, n * m == m * n.

Theorem NZmul_add_distr_r : forall n m p : NZ, (n + m) * p == n * p + m * p.

Theorem NZmul_add_distr_l : forall n m p : NZ, n * (m + p) == n * m + n * p.

Theorem NZmul_assoc : forall n m p : NZ, n * (m * p) == (n * m) * p.

Theorem NZmul_1_l : forall n : NZ, 1 * n == n.

Theorem NZmul_1_r : forall n : NZ, n * 1 == n.

End NZMulPropFunct.