Library Coq.Numbers.Integer.Abstract.ZAxioms
Require
Export
NZAxioms
.
Module
Type
ZAxiomsSig
.
Declare Module
Export
NZOrdAxiomsMod
:
NZOrdAxiomsSig
.
Delimit
Scope
IntScope
with
Int
.
Notation
Z
:=
NZ
.
Notation
Zeq
:=
NZeq
.
Notation
Z0
:=
NZ0
.
Notation
Z1
:= (
NZsucc
NZ0
).
Notation
S
:=
NZsucc
.
Notation
P
:=
NZpred
.
Notation
Zadd
:=
NZadd
.
Notation
Zmul
:=
NZmul
.
Notation
Zsub
:=
NZsub
.
Notation
Zlt
:=
NZlt
.
Notation
Zle
:=
NZle
.
Notation
Zmin
:=
NZmin
.
Notation
Zmax
:=
NZmax
.
Notation
"x == y" := (
NZeq
x
y
) (
at
level
70) :
IntScope
.
Notation
"x ~= y" := (~
NZeq
x
y
) (
at
level
70) :
IntScope
.
Notation
"0" :=
NZ0
:
IntScope
.
Notation
"1" := (
NZsucc
NZ0
) :
IntScope
.
Notation
"x + y" := (
NZadd
x
y
) :
IntScope
.
Notation
"x - y" := (
NZsub
x
y
) :
IntScope
.
Notation
"x * y" := (
NZmul
x
y
) :
IntScope
.
Notation
"x < y" := (
NZlt
x
y
) :
IntScope
.
Notation
"x <= y" := (
NZle
x
y
) :
IntScope
.
Notation
"x > y" := (
NZlt
y
x
) (
only
parsing
) :
IntScope
.
Notation
"x >= y" := (
NZle
y
x
) (
only
parsing
) :
IntScope
.
Parameter
Zopp
:
Z
->
Z
.
Add
Morphism
Zopp
with
signature
Zeq
==>
Zeq
as
Zopp_wd
.
Notation
"- x" := (
Zopp
x
) (
at
level
35,
right
associativity
) :
IntScope
.
Notation
"- 1" := (
Zopp
(
NZsucc
NZ0
)) :
IntScope
.
Open
Local
Scope
IntScope
.
Axiom
Zsucc_pred
:
forall
n
:
Z
,
S
(
P
n
) ==
n
.
Axiom
Zopp_0
: - 0 == 0.
Axiom
Zopp_succ
:
forall
n
:
Z
, - (
S
n
) ==
P
(-
n
).
End
ZAxiomsSig
.