Module nat_morphism

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.

Theorem pow_morphism: (x, y:nat)(pow x y)=(pow_nat x y).


Index
This page has been generated by coqdoc