Library Coq.Reals.Cauchy.ConstructiveExtra
Require
Import
ZArith
.
Require
Import
ConstructiveEpsilon
.
Definition
Z_inj_nat
(
z
:
Z
) :
nat
:=
match
z
with
|
Z0
=> 0
|
Zpos
p
=>
Pos.to_nat
(
p
~0
)
|
Zneg
p
=>
Pos.to_nat
(
Pos.pred_double
p
)
end
.
Definition
Z_inj_nat_rev
(
n
:
nat
) :
Z
:=
match
n
with
|
O
=> 0
|
S
n'
=>
match
Pos.of_nat
n
with
|
xH
=>
Zneg
xH
|
xO
p
=>
Zpos
p
|
xI
p
=>
Zneg
(
Pos.succ
p
)
end
end
.
Lemma
Pos_pred_double_inj
:
forall
(
p
q
:
positive
),
Pos.pred_double
p
=
Pos.pred_double
q
->
p
=
q
.
Lemma
Z_inj_nat_id
:
forall
(
z
:
Z
),
Z_inj_nat_rev
(
Z_inj_nat
z
)
=
z
.
Lemma
Z_inj_nat_inj
:
forall
(
x
y
:
Z
),
Z_inj_nat
x
=
Z_inj_nat
y
->
x
=
y
.
Lemma
constructive_indefinite_ground_description_Z
:
forall
P
:
Z
->
Prop
,
(
forall
z
:
Z
,
{
P
z
}
+
{
~
P
z
}
)
->
(
exists
z
:
Z
,
P
z
)
->
{
z
:
Z
|
P
z
}
.