Library Coq.ZArith.Zpow_def
Require
Import
ZArith_base
.
Require
Import
Ring_theory
.
Open
Local
Scope
Z_scope
.
Zpower_pos
z
n
is the n-th power of
z
when
n
is an binary integer (type
positive
) and
z
a signed integer (type
Z
)
Definition
Zpower_pos
(
z
:
Z
) (
n
:
positive
) :=
iter_pos
n
Z
(
fun
x
:
Z
=>
z
*
x
) 1.
Definition
Zpower
(
x
y
:
Z
) :=
match
y
with
|
Zpos
p
=>
Zpower_pos
x
p
|
Z0
=> 1
|
Zneg
p
=> 0
end
.
Lemma
Zpower_theory
:
power_theory
1
Zmult
(
eq
(
A
:=
Z
))
Z_of_N
Zpower
.