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
.