# Library Coq.NArith.Nnat

Require Import Arith_base.
Require Import Compare_dec.
Require Import Sumbool.
Require Import Div2.
Require Import Min.
Require Import Max.
Require Import BinPos.
Require Import BinNat.
Require Import BinInt.
Require Import Pnat.
Require Import Zmax.
Require Import Zmin.
Require Import Znat.

Translation from N to nat and back.

Definition nat_of_N (a:N) :=
match a with
| N0 => 0%nat
| Npos p => nat_of_P p
end.

Definition N_of_nat (n:nat) :=
match n with
| O => N0
| S n' => Npos (P_of_succ_nat n')
end.

Lemma N_of_nat_of_N : forall a:N, N_of_nat (nat_of_N a) = a.

Lemma nat_of_N_of_nat : forall n:nat, nat_of_N (N_of_nat n) = n.

Interaction of this translation and usual operations.

Lemma nat_of_Ndouble : forall a, nat_of_N (Ndouble a) = 2*(nat_of_N a).

Lemma N_of_double : forall n, N_of_nat (2*n) = Ndouble (N_of_nat n).

Lemma nat_of_Ndouble_plus_one :
forall a, nat_of_N (Ndouble_plus_one a) = S (2*(nat_of_N a)).

Lemma N_of_double_plus_one :
forall n, N_of_nat (S (2*n)) = Ndouble_plus_one (N_of_nat n).

Lemma nat_of_Nsucc : forall a, nat_of_N (Nsucc a) = S (nat_of_N a).

Lemma N_of_S : forall n, N_of_nat (S n) = Nsucc (N_of_nat n).

Lemma nat_of_Nplus :
forall a a', nat_of_N (Nplus a a') = (nat_of_N a)+(nat_of_N a').

Lemma N_of_plus :
forall n n', N_of_nat (n+n') = Nplus (N_of_nat n) (N_of_nat n').

Lemma nat_of_Nminus :
forall a a', nat_of_N (Nminus a a') = ((nat_of_N a)-(nat_of_N a'))%nat.

Lemma N_of_minus :
forall n n', N_of_nat (n-n') = Nminus (N_of_nat n) (N_of_nat n').

Lemma nat_of_Nmult :
forall a a', nat_of_N (Nmult a a') = (nat_of_N a)*(nat_of_N a').

Lemma N_of_mult :
forall n n', N_of_nat (n*n') = Nmult (N_of_nat n) (N_of_nat n').

Lemma nat_of_Ndiv2 :
forall a, nat_of_N (Ndiv2 a) = div2 (nat_of_N a).

Lemma N_of_div2 :
forall n, N_of_nat (div2 n) = Ndiv2 (N_of_nat n).

Lemma nat_of_Ncompare :
forall a a', Ncompare a a' = nat_compare (nat_of_N a) (nat_of_N a').

Lemma N_of_nat_compare :
forall n n', nat_compare n n' = Ncompare (N_of_nat n) (N_of_nat n').

Lemma nat_of_Nmin :
forall a a', nat_of_N (Nmin a a') = min (nat_of_N a) (nat_of_N a').

Lemma N_of_min :
forall n n', N_of_nat (min n n') = Nmin (N_of_nat n) (N_of_nat n').

Lemma nat_of_Nmax :
forall a a', nat_of_N (Nmax a a') = max (nat_of_N a) (nat_of_N a').

Lemma N_of_max :
forall n n', N_of_nat (max n n') = Nmax (N_of_nat n) (N_of_nat n').

Properties concerning Z_of_N

Lemma Z_of_nat_of_N : forall n:N, Z_of_nat (nat_of_N n) = Z_of_N n.

Lemma Z_of_N_eq : forall n m, n = m -> Z_of_N n = Z_of_N m.

Lemma Z_of_N_eq_rev : forall n m, Z_of_N n = Z_of_N m -> n = m.

Lemma Z_of_N_eq_iff : forall n m, n = m <-> Z_of_N n = Z_of_N m.

Lemma Z_of_N_le : forall n m, (n<=m)%N -> (Z_of_N n <= Z_of_N m)%Z.

Lemma Z_of_N_le_rev : forall n m, (Z_of_N n <= Z_of_N m)%Z -> (n<=m)%N.

Lemma Z_of_N_le_iff : forall n m, (n<=m)%N <-> (Z_of_N n <= Z_of_N m)%Z.

Lemma Z_of_N_lt : forall n m, (n<m)%N -> (Z_of_N n < Z_of_N m)%Z.

Lemma Z_of_N_lt_rev : forall n m, (Z_of_N n < Z_of_N m)%Z -> (n<m)%N.

Lemma Z_of_N_lt_iff : forall n m, (n<m)%N <-> (Z_of_N n < Z_of_N m)%Z.

Lemma Z_of_N_ge : forall n m, (n>=m)%N -> (Z_of_N n >= Z_of_N m)%Z.

Lemma Z_of_N_ge_rev : forall n m, (Z_of_N n >= Z_of_N m)%Z -> (n>=m)%N.

Lemma Z_of_N_ge_iff : forall n m, (n>=m)%N <-> (Z_of_N n >= Z_of_N m)%Z.

Lemma Z_of_N_gt : forall n m, (n>m)%N -> (Z_of_N n > Z_of_N m)%Z.

Lemma Z_of_N_gt_rev : forall n m, (Z_of_N n > Z_of_N m)%Z -> (n>m)%N.

Lemma Z_of_N_gt_iff : forall n m, (n>m)%N <-> (Z_of_N n > Z_of_N m)%Z.

Lemma Z_of_N_of_nat : forall n:nat, Z_of_N (N_of_nat n) = Z_of_nat n.

Lemma Z_of_N_pos : forall p:positive, Z_of_N (Npos p) = Zpos p.

Lemma Z_of_N_abs : forall z:Z, Z_of_N (Zabs_N z) = Zabs z.

Lemma Z_of_N_le_0 : forall n, (0 <= Z_of_N n)%Z.

Lemma Z_of_N_plus : forall n m:N, Z_of_N (n+m) = (Z_of_N n + Z_of_N m)%Z.

Lemma Z_of_N_mult : forall n m:N, Z_of_N (n*m) = (Z_of_N n * Z_of_N m)%Z.

Lemma Z_of_N_minus : forall n m:N, Z_of_N (n-m) = Zmax 0 (Z_of_N n - Z_of_N m).

Lemma Z_of_N_succ : forall n:N, Z_of_N (Nsucc n) = Zsucc (Z_of_N n).

Lemma Z_of_N_min : forall n m:N, Z_of_N (Nmin n m) = Zmin (Z_of_N n) (Z_of_N m).

Lemma Z_of_N_max : forall n m:N, Z_of_N (Nmax n m) = Zmax (Z_of_N n) (Z_of_N m).