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