Library Coq.NArith.Nnat
Translation from N to nat and back.
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).