Require Export ZArith.
Require Export Omega.
Require Export pow.
Coercion inject_nat : nat >-> Z.
Theorem add_un_add: (p:positive)(add_un p)=(add xH p).
Theorem S_morphism: (a:nat)<Z> (S a)=(Zplus a (POS xH)).
Theorem plus_morphism: (a, b:nat)(Zplus a b)=(plus a b).
Theorem mult_morphism: (a, b:nat)(Zmult a b)=(mult a b).
Theorem le_Zle: (a, b:nat) (le a b) ->(Zle a b).
Fixpoint pow_nat[x, y:nat]: nat :=
Cases y of
O => (1)
| (S p) => (mult x (pow_nat x p))
end.