# 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.