Library Coq.Numbers.Natural.Abstract.NAxioms
Require
Export
NZAxioms
.
Module
Type
NAxioms
(
Import
NZ
:
NZDomainSig'
).
Axiom
pred_0
:
P
0
==
0.
Parameter
Inline
recursion
:
forall
A
:
Type
,
A
-> (
t
->
A
->
A
) ->
t
->
A
.
Implicit Arguments
recursion
[
A
].
Declare Instance
recursion_wd
(
A
:
Type
) (
Aeq
:
relation
A
) :
Proper
(
Aeq
==>
(
eq
==>
Aeq
==>
Aeq
)
==>
eq
==>
Aeq
) (@
recursion
A
).
Axiom
recursion_0
:
forall
(
A
:
Type
) (
a
:
A
) (
f
:
t
->
A
->
A
),
recursion
a
f
0
=
a
.
Axiom
recursion_succ
:
forall
(
A
:
Type
) (
Aeq
:
relation
A
) (
a
:
A
) (
f
:
t
->
A
->
A
),
Aeq
a
a
->
Proper
(
eq
==>
Aeq
==>
Aeq
)
f
->
forall
n
,
Aeq
(
recursion
a
f
(
S
n
)) (
f
n
(
recursion
a
f
n
)).
End
NAxioms
.
Module
Type
NAxiomsSig
:=
NZOrdAxiomsSig
<+
NAxioms
.
Module
Type
NAxiomsSig'
:=
NZOrdAxiomsSig'
<+
NAxioms
.