Library Coq.Numbers.NatInt.NZBase
Require
Import
NZAxioms
.
Module
NZBasePropFunct
(
Import
NZAxiomsMod
:
NZAxiomsSig
).
Open
Local
Scope
NatIntScope
.
Theorem
NZneq_sym
:
forall
n
m
:
NZ
,
n
~=
m
->
m
~=
n
.
Theorem
NZE_stepl
:
forall
x
y
z
:
NZ
,
x
==
y
->
x
==
z
->
z
==
y
.
Declare Left Step
NZE_stepl
.
Declare Right Step
(
proj1
(
proj2
NZeq_equiv
)).
Theorem
NZsucc_inj
:
forall
n1
n2
:
NZ
,
S
n1
==
S
n2
->
n1
==
n2
.
Theorem
NZsucc_inj_wd
:
forall
n1
n2
:
NZ
,
S
n1
==
S
n2
<->
n1
==
n2
.
Theorem
NZsucc_inj_wd_neg
:
forall
n
m
:
NZ
,
S
n
~=
S
m
<->
n
~=
m
.
Section
CentralInduction
.
Variable
A
:
predicate
NZ
.
Hypothesis
A_wd
:
predicate_wd
NZeq
A
.
Add
Morphism
A
with
signature
NZeq
==>
iff
as
A_morph
.
Theorem
NZcentral_induction
:
forall
z
:
NZ
,
A
z
->
(
forall
n
:
NZ
,
A
n
<->
A
(
S
n
)) ->
forall
n
:
NZ
,
A
n
.
End
CentralInduction
.
Tactic Notation
"NZinduct"
ident
(
n
) :=
induction_maker
n
ltac
:(apply
NZinduction
).
Tactic Notation
"NZinduct"
ident
(
n
)
constr
(
u
) :=
induction_maker
n
ltac
:(apply
NZcentral_induction
with
(
z
:=
u
)).
End
NZBasePropFunct
.