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
.