Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(* -*- coding: utf-8 -*- *)
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Binary Integers (Pierre Crégut, CNET, Lannion, France)

Require Export Arith_base.
Require Import BinPos BinInt BinNat Pnat Nnat.

Local Open Scope Z_scope.

Conversions between integers and natural numbers

Seven sections:

chains of conversions (combining two conversions)
module N2Z : from N to Z
module Z2N : from Z to N (negative numbers rounded to 0)
module Zabs2N : from Z to N (via the absolute value)
module Nat2Z : from nat to Z
module Z2Nat : from Z to nat (negative numbers rounded to 0)
module Zabs2Nat : from Z to nat (via the absolute value)

Chains of conversions

When combining successive conversions, we have the following commutative diagram:

      ---> Nat ----
     |      ^      |
     |      |      v
    Pos ---------> Z
     |      |      ^
     |      v      |
      ----> N -----

Lemma nat_N_Z n : Z.of_N (N.of_nat n) = Z.of_nat n.n:nat
Z.of_N (N.of_nat n) = Z.of_nat n
Proof.n:nat
Z.of_N (N.of_nat n) = Z.of_nat n
 now destruct n.
Qed.

Lemma N_nat_Z n : Z.of_nat (N.to_nat n) = Z.of_N n.n:N
Z.of_nat (N.to_nat n) = Z.of_N n
Proof.n:N
Z.of_nat (N.to_nat n) = Z.of_N n
 destruct n; trivial.p:positive
Z.of_nat (N.to_nat (N.pos p)) = Z.of_N (N.pos p) simpl.p:positive
Z.of_nat (Pos.to_nat p) = Z.pos p
 destruct (Pos2Nat.is_succ p) as (m,H).p:positive
m:nat
H:Pos.to_nat p = S m
Z.of_nat (Pos.to_nat p) = Z.pos p
 rewrite H.p:positive
m:nat
H:Pos.to_nat p = S m
Z.of_nat (S m) = Z.pos p simpl.p:positive
m:nat
H:Pos.to_nat p = S m
Z.pos (Pos.of_succ_nat m) = Z.pos p f_equal.p:positive
m:nat
H:Pos.to_nat p = S m
Pos.of_succ_nat m = p now apply SuccNat2Pos.inv.
Qed.

Lemma positive_nat_Z p : Z.of_nat (Pos.to_nat p) = Zpos p.p:positive
Z.of_nat (Pos.to_nat p) = Z.pos p
Proof.p:positive
Z.of_nat (Pos.to_nat p) = Z.pos p
 destruct (Pos2Nat.is_succ p) as (n,H).p:positive
n:nat
H:Pos.to_nat p = S n
Z.of_nat (Pos.to_nat p) = Z.pos p
 rewrite H.p:positive
n:nat
H:Pos.to_nat p = S n
Z.of_nat (S n) = Z.pos p simpl.p:positive
n:nat
H:Pos.to_nat p = S n
Z.pos (Pos.of_succ_nat n) = Z.pos p f_equal.p:positive
n:nat
H:Pos.to_nat p = S n
Pos.of_succ_nat n = p now apply SuccNat2Pos.inv.
Qed.

Lemma positive_N_Z p : Z.of_N (Npos p) = Zpos p.p:positive
Z.of_N (N.pos p) = Z.pos p
Proof.p:positive
Z.of_N (N.pos p) = Z.pos p
 reflexivity.
Qed.

Lemma positive_N_nat p : N.to_nat (Npos p) = Pos.to_nat p.p:positive
N.to_nat (N.pos p) = Pos.to_nat p
Proof.p:positive
N.to_nat (N.pos p) = Pos.to_nat p
 reflexivity.
Qed.

Lemma positive_nat_N p : N.of_nat (Pos.to_nat p) = Npos p.p:positive
N.of_nat (Pos.to_nat p) = N.pos p
Proof.p:positive
N.of_nat (Pos.to_nat p) = N.pos p
 destruct (Pos2Nat.is_succ p) as (n,H).p:positive
n:nat
H:Pos.to_nat p = S n
N.of_nat (Pos.to_nat p) = N.pos p
 rewrite H.p:positive
n:nat
H:Pos.to_nat p = S n
N.of_nat (S n) = N.pos p simpl.p:positive
n:nat
H:Pos.to_nat p = S n
N.pos (Pos.of_succ_nat n) = N.pos p f_equal.p:positive
n:nat
H:Pos.to_nat p = S n
Pos.of_succ_nat n = p now apply SuccNat2Pos.inv.
Qed.

Lemma Z_N_nat n : N.to_nat (Z.to_N n) = Z.to_nat n.n:Z
N.to_nat (Z.to_N n) = Z.to_nat n
Proof.n:Z
N.to_nat (Z.to_N n) = Z.to_nat n
 now destruct n.
Qed.

Lemma Z_nat_N n : N.of_nat (Z.to_nat n) = Z.to_N n.n:Z
N.of_nat (Z.to_nat n) = Z.to_N n
Proof.n:Z
N.of_nat (Z.to_nat n) = Z.to_N n
 destruct n; simpl; trivial.p:positive
N.of_nat (Pos.to_nat p) = N.pos p apply positive_nat_N.
Qed.

Lemma Zabs_N_nat n : N.to_nat (Z.abs_N n) = Z.abs_nat n.n:Z
N.to_nat (Z.abs_N n) = Z.abs_nat n
Proof.n:Z
N.to_nat (Z.abs_N n) = Z.abs_nat n
 now destruct n.
Qed.

Lemma Zabs_nat_N n : N.of_nat (Z.abs_nat n) = Z.abs_N n.n:Z
N.of_nat (Z.abs_nat n) = Z.abs_N n
Proof.n:Z
N.of_nat (Z.abs_nat n) = Z.abs_N n
 destruct n; simpl; trivial; apply positive_nat_N.
Qed.

Conversions between Z and N

Module N2Z.

Z.of_N is a bijection between N and non-negative Z, with Z.to_N (or Z.abs_N) as reciprocal. See Z2N.id below for the dual equation.

Lemma id n : Z.to_N (Z.of_N n) = n.n:N
Z.to_N (Z.of_N n) = n
Proof.n:N
Z.to_N (Z.of_N n) = n
 now destruct n.
Qed.

Z.of_N is hence injective

Lemma inj n m : Z.of_N n = Z.of_N m -> n = m.n, m:N
Z.of_N n = Z.of_N m -> n = m
Proof.n, m:N
Z.of_N n = Z.of_N m -> n = m
 destruct n, m; simpl; congruence.
Qed.

Lemma inj_iff n m : Z.of_N n = Z.of_N m <-> n = m.n, m:N
Z.of_N n = Z.of_N m <-> n = m
Proof.n, m:N
Z.of_N n = Z.of_N m <-> n = m
 split.n, m:N
Z.of_N n = Z.of_N m -> n = m
n, m:N
n = m -> Z.of_N n = Z.of_N m apply inj.n, m:N
n = m -> Z.of_N n = Z.of_N m intros; now f_equal.
Qed.

Z.of_N produce non-negative integers

Lemma is_nonneg n : 0 <= Z.of_N n.n:N
0 <= Z.of_N n
Proof.n:N
0 <= Z.of_N n
 now destruct n.
Qed.

Z.of_N, basic equations

Lemma inj_0 : Z.of_N 0 = 0.Z.of_N 0 = 0
Proof.Z.of_N 0 = 0
 reflexivity.
Qed.

Lemma inj_pos p : Z.of_N (Npos p) = Zpos p.p:positive
Z.of_N (N.pos p) = Z.pos p
Proof.p:positive
Z.of_N (N.pos p) = Z.pos p
 reflexivity.
Qed.

Z.of_N and usual operations.

Lemma inj_compare n m : (Z.of_N n ?= Z.of_N m) = (n ?= m)%N.n, m:N
(Z.of_N n ?= Z.of_N m) = (n ?= m)%N
Proof.n, m:N
(Z.of_N n ?= Z.of_N m) = (n ?= m)%N
 now destruct n, m.
Qed.

Lemma inj_le n m : (n<=m)%N <-> Z.of_N n <= Z.of_N m.n, m:N
(n <= m)%N <-> Z.of_N n <= Z.of_N m
Proof.n, m:N
(n <= m)%N <-> Z.of_N n <= Z.of_N m
 unfold Z.le.n, m:N
(n <= m)%N <-> (Z.of_N n ?= Z.of_N m) <> Gt now rewrite inj_compare.
Qed.

Lemma inj_lt n m : (n<m)%N <-> Z.of_N n < Z.of_N m.n, m:N
(n < m)%N <-> Z.of_N n < Z.of_N m
Proof.n, m:N
(n < m)%N <-> Z.of_N n < Z.of_N m
 unfold Z.lt.n, m:N
(n < m)%N <-> (Z.of_N n ?= Z.of_N m) = Lt now rewrite inj_compare.
Qed.

Lemma inj_ge n m : (n>=m)%N <-> Z.of_N n >= Z.of_N m.n, m:N
(n >= m)%N <-> Z.of_N n >= Z.of_N m
Proof.n, m:N
(n >= m)%N <-> Z.of_N n >= Z.of_N m
 unfold Z.ge.n, m:N
(n >= m)%N <-> (Z.of_N n ?= Z.of_N m) <> Lt now rewrite inj_compare.
Qed.

Lemma inj_gt n m : (n>m)%N <-> Z.of_N n > Z.of_N m.n, m:N
(n > m)%N <-> Z.of_N n > Z.of_N m
Proof.n, m:N
(n > m)%N <-> Z.of_N n > Z.of_N m
 unfold Z.gt.n, m:N
(n > m)%N <-> (Z.of_N n ?= Z.of_N m) = Gt now rewrite inj_compare.
Qed.

Lemma inj_abs_N z : Z.of_N (Z.abs_N z) = Z.abs z.z:Z
Z.of_N (Z.abs_N z) = Z.abs z
Proof.z:Z
Z.of_N (Z.abs_N z) = Z.abs z
 now destruct z.
Qed.

Lemma inj_add n m : Z.of_N (n+m) = Z.of_N n + Z.of_N m.n, m:N
Z.of_N (n + m) = Z.of_N n + Z.of_N m
Proof.n, m:N
Z.of_N (n + m) = Z.of_N n + Z.of_N m
 now destruct n, m.
Qed.

Lemma inj_mul n m : Z.of_N (n*m) = Z.of_N n * Z.of_N m.n, m:N
Z.of_N (n * m) = Z.of_N n * Z.of_N m
Proof.n, m:N
Z.of_N (n * m) = Z.of_N n * Z.of_N m
 now destruct n, m.
Qed.

Lemma inj_sub_max n m : Z.of_N (n-m) = Z.max 0 (Z.of_N n - Z.of_N m).n, m:N
Z.of_N (n - m) = Z.max 0 (Z.of_N n - Z.of_N m)
Proof.n, m:N
Z.of_N (n - m) = Z.max 0 (Z.of_N n - Z.of_N m)
 destruct n as [|n], m as [|m]; simpl; trivial.n, m:positive
Z.of_N
  match Pos.sub_mask n m with
  | Pos.IsPos p => N.pos p
  | _ => 0
  end = Z.max 0 (Z.pos_sub n m)
 rewrite Z.pos_sub_spec, Pos.compare_sub_mask.n, m:positive
Z.of_N
  match Pos.sub_mask n m with
  | Pos.IsPos p => N.pos p
  | _ => 0
  end =
Z.max 0
  match Pos.mask2cmp (Pos.sub_mask n m) with
  | Eq => 0
  | Lt => Z.neg (m - n)
  | Gt => Z.pos (n - m)
  end unfold Pos.sub.n, m:positive
Z.of_N
  match Pos.sub_mask n m with
  | Pos.IsPos p => N.pos p
  | _ => 0
  end =
Z.max 0
  match Pos.mask2cmp (Pos.sub_mask n m) with
  | Eq => 0
  | Lt =>
      Z.neg
        match Pos.sub_mask m n with
        | Pos.IsPos z => z
        | _ => 1
        end
  | Gt =>
      Z.pos
        match Pos.sub_mask n m with
        | Pos.IsPos z => z
        | _ => 1
        end
  end
 now destruct (Pos.sub_mask n m).
Qed.

Lemma inj_sub n m : (m<=n)%N -> Z.of_N (n-m) = Z.of_N n - Z.of_N m.n, m:N
(m <= n)%N -> Z.of_N (n - m) = Z.of_N n - Z.of_N m
Proof.n, m:N
(m <= n)%N -> Z.of_N (n - m) = Z.of_N n - Z.of_N m
 intros H.n, m:N
H:(m <= n)%N
Z.of_N (n - m) = Z.of_N n - Z.of_N m rewrite inj_sub_max.n, m:N
H:(m <= n)%N
Z.max 0 (Z.of_N n - Z.of_N m) = Z.of_N n - Z.of_N m
 unfold N.le in H.n, m:N
H:(m ?= n)%N <> Gt
Z.max 0 (Z.of_N n - Z.of_N m) = Z.of_N n - Z.of_N m
 rewrite N.compare_antisym, <- inj_compare, Z.compare_sub in H.n, m:N
H:CompOpp (Z.of_N n - Z.of_N m ?= 0) <> Gt
Z.max 0 (Z.of_N n - Z.of_N m) = Z.of_N n - Z.of_N m
 destruct (Z.of_N n - Z.of_N m); trivial; now destruct H.
Qed.

Lemma inj_succ n : Z.of_N (N.succ n) = Z.succ (Z.of_N n).n:N
Z.of_N (N.succ n) = Z.succ (Z.of_N n)
Proof.n:N
Z.of_N (N.succ n) = Z.succ (Z.of_N n)
 destruct n.Z.of_N (N.succ 0) = Z.succ (Z.of_N 0)
p:positive
Z.of_N (N.succ (N.pos p)) = Z.succ (Z.of_N (N.pos p)) trivial.p:positive
Z.of_N (N.succ (N.pos p)) = Z.succ (Z.of_N (N.pos p)) simpl.p:positive
Z.pos (Pos.succ p) = Z.pos (p + 1) now rewrite Pos.add_1_r.
Qed.

Lemma inj_pred_max n : Z.of_N (N.pred n) = Z.max 0 (Z.pred (Z.of_N n)).n:N
Z.of_N (N.pred n) = Z.max 0 (Z.pred (Z.of_N n))
Proof.n:N
Z.of_N (N.pred n) = Z.max 0 (Z.pred (Z.of_N n))
 unfold Z.pred.n:N
Z.of_N (N.pred n) = Z.max 0 (Z.of_N n + -1) now rewrite N.pred_sub, inj_sub_max.
Qed.

Lemma inj_pred n : (0<n)%N -> Z.of_N (N.pred n) = Z.pred (Z.of_N n).n:N
(0 < n)%N -> Z.of_N (N.pred n) = Z.pred (Z.of_N n)
Proof.n:N
(0 < n)%N -> Z.of_N (N.pred n) = Z.pred (Z.of_N n)
 intros H.n:N
H:(0 < n)%N
Z.of_N (N.pred n) = Z.pred (Z.of_N n) unfold Z.pred.n:N
H:(0 < n)%N
Z.of_N (N.pred n) = Z.of_N n + -1 rewrite N.pred_sub, inj_sub; trivial.n:N
H:(0 < n)%N
(1 <= n)%N
 now apply N.le_succ_l in H.
Qed.

Lemma inj_min n m : Z.of_N (N.min n m) = Z.min (Z.of_N n) (Z.of_N m).n, m:N
Z.of_N (N.min n m) = Z.min (Z.of_N n) (Z.of_N m)
Proof.n, m:N
Z.of_N (N.min n m) = Z.min (Z.of_N n) (Z.of_N m)
 unfold Z.min, N.min.n, m:N
Z.of_N match (n ?= m)%N with
       | Gt => m
       | _ => n
       end =
match Z.of_N n ?= Z.of_N m with
| Gt => Z.of_N m
| _ => Z.of_N n
end rewrite inj_compare.n, m:N
Z.of_N match (n ?= m)%N with
       | Gt => m
       | _ => n
       end =
match (n ?= m)%N with
| Gt => Z.of_N m
| _ => Z.of_N n
end now case N.compare.
Qed.

Lemma inj_max n m : Z.of_N (N.max n m) = Z.max (Z.of_N n) (Z.of_N m).n, m:N
Z.of_N (N.max n m) = Z.max (Z.of_N n) (Z.of_N m)
Proof.n, m:N
Z.of_N (N.max n m) = Z.max (Z.of_N n) (Z.of_N m)
 unfold Z.max, N.max.n, m:N
Z.of_N match (n ?= m)%N with
       | Gt => n
       | _ => m
       end =
match Z.of_N n ?= Z.of_N m with
| Lt => Z.of_N m
| _ => Z.of_N n
end rewrite inj_compare.n, m:N
Z.of_N match (n ?= m)%N with
       | Gt => n
       | _ => m
       end =
match (n ?= m)%N with
| Lt => Z.of_N m
| _ => Z.of_N n
end
 case N.compare_spec; intros; subst; trivial.
Qed.

Lemma inj_div n m : Z.of_N (n/m) = Z.of_N n / Z.of_N m.n, m:N
Z.of_N (n / m) = Z.of_N n / Z.of_N m
Proof.n, m:N
Z.of_N (n / m) = Z.of_N n / Z.of_N m
 destruct m as [|m].n:N
Z.of_N (n / 0) = Z.of_N n / Z.of_N 0
n:N
m:positive
Z.of_N (n / N.pos m) = Z.of_N n / Z.of_N (N.pos m) now destruct n.n:N
m:positive
Z.of_N (n / N.pos m) = Z.of_N n / Z.of_N (N.pos m)
 apply Z.div_unique_pos with (Z.of_N (n mod (Npos m))).n:N
m:positive
0 <= Z.of_N (n mod N.pos m) < Z.of_N (N.pos m)
n:N
m:positive
Z.of_N n =
Z.of_N (N.pos m) * Z.of_N (n / N.pos m) +
Z.of_N (n mod N.pos m)
 split.n:N
m:positive
0 <= Z.of_N (n mod N.pos m)
n:N
m:positive
Z.of_N (n mod N.pos m) < Z.of_N (N.pos m)
n:N
m:positive
Z.of_N n =
Z.of_N (N.pos m) * Z.of_N (n / N.pos m) +
Z.of_N (n mod N.pos m) apply is_nonneg.n:N
m:positive
Z.of_N (n mod N.pos m) < Z.of_N (N.pos m)
n:N
m:positive
Z.of_N n =
Z.of_N (N.pos m) * Z.of_N (n / N.pos m) +
Z.of_N (n mod N.pos m) apply inj_lt.n:N
m:positive
(n mod N.pos m < N.pos m)%N
n:N
m:positive
Z.of_N n =
Z.of_N (N.pos m) * Z.of_N (n / N.pos m) +
Z.of_N (n mod N.pos m) now apply N.mod_lt.n:N
m:positive
Z.of_N n =
Z.of_N (N.pos m) * Z.of_N (n / N.pos m) +
Z.of_N (n mod N.pos m)
 rewrite <- inj_mul, <- inj_add.n:N
m:positive
Z.of_N n =
Z.of_N (N.pos m * (n / N.pos m) + n mod N.pos m) f_equal.n:N
m:positive
n = (N.pos m * (n / N.pos m) + n mod N.pos m)%N now apply N.div_mod.
Qed.

Lemma inj_mod n m : (m<>0)%N -> Z.of_N (n mod m) = (Z.of_N n) mod (Z.of_N m).n, m:N
m <> 0%N -> Z.of_N (n mod m) = Z.of_N n mod Z.of_N m
Proof.n, m:N
m <> 0%N -> Z.of_N (n mod m) = Z.of_N n mod Z.of_N m
 intros Hm.n, m:N
Hm:m <> 0%N
Z.of_N (n mod m) = Z.of_N n mod Z.of_N m
 apply Z.mod_unique_pos with (Z.of_N (n / m)).n, m:N
Hm:m <> 0%N
0 <= Z.of_N (n mod m) < Z.of_N m
n, m:N
Hm:m <> 0%N
Z.of_N n =
Z.of_N m * Z.of_N (n / m) + Z.of_N (n mod m)
 split.n, m:N
Hm:m <> 0%N
0 <= Z.of_N (n mod m)
n, m:N
Hm:m <> 0%N
Z.of_N (n mod m) < Z.of_N m
n, m:N
Hm:m <> 0%N
Z.of_N n =
Z.of_N m * Z.of_N (n / m) + Z.of_N (n mod m) apply is_nonneg.n, m:N
Hm:m <> 0%N
Z.of_N (n mod m) < Z.of_N m
n, m:N
Hm:m <> 0%N
Z.of_N n =
Z.of_N m * Z.of_N (n / m) + Z.of_N (n mod m) apply inj_lt.n, m:N
Hm:m <> 0%N
(n mod m < m)%N
n, m:N
Hm:m <> 0%N
Z.of_N n =
Z.of_N m * Z.of_N (n / m) + Z.of_N (n mod m) now apply N.mod_lt.n, m:N
Hm:m <> 0%N
Z.of_N n =
Z.of_N m * Z.of_N (n / m) + Z.of_N (n mod m)
 rewrite <- inj_mul, <- inj_add.n, m:N
Hm:m <> 0%N
Z.of_N n = Z.of_N (m * (n / m) + n mod m) f_equal.n, m:N
Hm:m <> 0%N
n = (m * (n / m) + n mod m)%N now apply N.div_mod.
Qed.

Lemma inj_quot n m : Z.of_N (n/m) = Z.of_N n ÷ Z.of_N m.n, m:N
Z.of_N (n / m) = Z.of_N n ÷ Z.of_N m
Proof.n, m:N
Z.of_N (n / m) = Z.of_N n ÷ Z.of_N m
 destruct m.n:N
Z.of_N (n / 0) = Z.of_N n ÷ Z.of_N 0
n:N
p:positive
Z.of_N (n / N.pos p) = Z.of_N n ÷ Z.of_N (N.pos p)
 -n:N
Z.of_N (n / 0) = Z.of_N n ÷ Z.of_N 0 now destruct n.
 -n:N
p:positive
Z.of_N (n / N.pos p) = Z.of_N n ÷ Z.of_N (N.pos p) rewrite Z.quot_div_nonneg, inj_div; trivial.n:N
p:positive
0 <= Z.of_N n
n:N
p:positive
0 < Z.of_N (N.pos p) apply is_nonneg.n:N
p:positive
0 < Z.of_N (N.pos p) easy.
Qed.

Lemma inj_rem n m : Z.of_N (n mod m) = Z.rem (Z.of_N n) (Z.of_N m).n, m:N
Z.of_N (n mod m) = Z.rem (Z.of_N n) (Z.of_N m)
Proof.n, m:N
Z.of_N (n mod m) = Z.rem (Z.of_N n) (Z.of_N m)
 destruct m.n:N
Z.of_N (n mod 0) = Z.rem (Z.of_N n) (Z.of_N 0)
n:N
p:positive
Z.of_N (n mod N.pos p) =
Z.rem (Z.of_N n) (Z.of_N (N.pos p))
 -n:N
Z.of_N (n mod 0) = Z.rem (Z.of_N n) (Z.of_N 0) now destruct n.
 -n:N
p:positive
Z.of_N (n mod N.pos p) =
Z.rem (Z.of_N n) (Z.of_N (N.pos p)) rewrite Z.rem_mod_nonneg, inj_mod; trivial.n:N
p:positive
N.pos p <> 0%N
n:N
p:positive
0 <= Z.of_N n
n:N
p:positive
0 < Z.of_N (N.pos p) easy.n:N
p:positive
0 <= Z.of_N n
n:N
p:positive
0 < Z.of_N (N.pos p) apply is_nonneg.n:N
p:positive
0 < Z.of_N (N.pos p) easy.
Qed.

Lemma inj_div2 n : Z.of_N (N.div2 n) = Z.div2 (Z.of_N n).n:N
Z.of_N (N.div2 n) = Z.div2 (Z.of_N n)
Proof.n:N
Z.of_N (N.div2 n) = Z.div2 (Z.of_N n)
 destruct n as [|p]; trivial.p:positive
Z.of_N (N.div2 (N.pos p)) = Z.div2 (Z.of_N (N.pos p)) now destruct p.
Qed.

Lemma inj_quot2 n : Z.of_N (N.div2 n) = Z.quot2 (Z.of_N n).n:N
Z.of_N (N.div2 n) = Z.quot2 (Z.of_N n)
Proof.n:N
Z.of_N (N.div2 n) = Z.quot2 (Z.of_N n)
 destruct n as [|p]; trivial.p:positive
Z.of_N (N.div2 (N.pos p)) = Z.quot2 (Z.of_N (N.pos p)) now destruct p.
Qed.

Lemma inj_pow n m : Z.of_N (n^m) = (Z.of_N n)^(Z.of_N m).n, m:N
Z.of_N (n ^ m) = Z.of_N n ^ Z.of_N m
Proof.n, m:N
Z.of_N (n ^ m) = Z.of_N n ^ Z.of_N m
 destruct n, m; trivial.p:positive
Z.of_N (0 ^ N.pos p) = Z.of_N 0 ^ Z.of_N (N.pos p)
p, p0:positive
Z.of_N (N.pos p ^ N.pos p0) =
Z.of_N (N.pos p) ^ Z.of_N (N.pos p0) now rewrite Z.pow_0_l.p, p0:positive
Z.of_N (N.pos p ^ N.pos p0) =
Z.of_N (N.pos p) ^ Z.of_N (N.pos p0) apply Pos2Z.inj_pow.
Qed.

Lemma inj_testbit a n :
 Z.testbit (Z.of_N a) (Z.of_N n) = N.testbit a n.a, n:N
Z.testbit (Z.of_N a) (Z.of_N n) = N.testbit a n
Proof.a, n:N
Z.testbit (Z.of_N a) (Z.of_N n) = N.testbit a n apply Z.testbit_of_N. Qed.

End N2Z.

Module Z2N.

Z.to_N is a bijection between non-negative Z and N, with Pos.of_N as reciprocal. See N2Z.id above for the dual equation.

Lemma id n : 0<=n -> Z.of_N (Z.to_N n) = n.n:Z
0 <= n -> Z.of_N (Z.to_N n) = n
Proof.n:Z
0 <= n -> Z.of_N (Z.to_N n) = n
 destruct n; (now destruct 1) || trivial.
Qed.

Z.to_N is hence injective for non-negative integers.

Lemma inj n m : 0<=n -> 0<=m -> Z.to_N n = Z.to_N m -> n = m.n, m:Z
0 <= n -> 0 <= m -> Z.to_N n = Z.to_N m -> n = m
Proof.n, m:Z
0 <= n -> 0 <= m -> Z.to_N n = Z.to_N m -> n = m
 intros.n, m:Z
H:0 <= n
H0:0 <= m
H1:Z.to_N n = Z.to_N m
n = m rewrite <- (id n), <- (id m) by trivial.n, m:Z
H:0 <= n
H0:0 <= m
H1:Z.to_N n = Z.to_N m
Z.of_N (Z.to_N n) = Z.of_N (Z.to_N m) now f_equal.
Qed.

Lemma inj_iff n m : 0<=n -> 0<=m -> (Z.to_N n = Z.to_N m <-> n = m).n, m:Z
0 <= n -> 0 <= m -> Z.to_N n = Z.to_N m <-> n = m
Proof.n, m:Z
0 <= n -> 0 <= m -> Z.to_N n = Z.to_N m <-> n = m
 intros.n, m:Z
H:0 <= n
H0:0 <= m
Z.to_N n = Z.to_N m <-> n = m split.n, m:Z
H:0 <= n
H0:0 <= m
Z.to_N n = Z.to_N m -> n = m
n, m:Z
H:0 <= n
H0:0 <= m
n = m -> Z.to_N n = Z.to_N m now apply inj.n, m:Z
H:0 <= n
H0:0 <= m
n = m -> Z.to_N n = Z.to_N m intros; now subst.
Qed.

Z.to_N, basic equations

Lemma inj_0 : Z.to_N 0 = 0%N.Z.to_N 0 = 0%N
Proof.Z.to_N 0 = 0%N
 reflexivity.
Qed.

Lemma inj_pos n : Z.to_N (Zpos n) = Npos n.n:positive
Z.to_N (Z.pos n) = N.pos n
Proof.n:positive
Z.to_N (Z.pos n) = N.pos n
 reflexivity.
Qed.

Lemma inj_neg n : Z.to_N (Zneg n) = 0%N.n:positive
Z.to_N (Z.neg n) = 0%N
Proof.n:positive
Z.to_N (Z.neg n) = 0%N
 reflexivity.
Qed.

Z.to_N and operations

Lemma inj_add n m : 0<=n -> 0<=m -> Z.to_N (n+m) = (Z.to_N n + Z.to_N m)%N.n, m:Z
0 <= n ->
0 <= m -> Z.to_N (n + m) = (Z.to_N n + Z.to_N m)%N
Proof.n, m:Z
0 <= n ->
0 <= m -> Z.to_N (n + m) = (Z.to_N n + Z.to_N m)%N
 destruct n, m; trivial; (now destruct 1) || (now destruct 2).
Qed.

Lemma inj_mul n m : 0<=n -> 0<=m -> Z.to_N (n*m) = (Z.to_N n * Z.to_N m)%N.n, m:Z
0 <= n ->
0 <= m -> Z.to_N (n * m) = (Z.to_N n * Z.to_N m)%N
Proof.n, m:Z
0 <= n ->
0 <= m -> Z.to_N (n * m) = (Z.to_N n * Z.to_N m)%N
 destruct n, m; trivial; (now destruct 1) || (now destruct 2).
Qed.

Lemma inj_succ n : 0<=n -> Z.to_N (Z.succ n) = N.succ (Z.to_N n).n:Z
0 <= n -> Z.to_N (Z.succ n) = N.succ (Z.to_N n)
Proof.n:Z
0 <= n -> Z.to_N (Z.succ n) = N.succ (Z.to_N n)
 unfold Z.succ.n:Z
0 <= n -> Z.to_N (n + 1) = N.succ (Z.to_N n) intros.n:Z
H:0 <= n
Z.to_N (n + 1) = N.succ (Z.to_N n) rewrite inj_add by easy.n:Z
H:0 <= n
(Z.to_N n + Z.to_N 1)%N = N.succ (Z.to_N n) apply N.add_1_r.
Qed.

Lemma inj_sub n m : 0<=m -> Z.to_N (n - m) = (Z.to_N n - Z.to_N m)%N.n, m:Z
0 <= m -> Z.to_N (n - m) = (Z.to_N n - Z.to_N m)%N
Proof.n, m:Z
0 <= m -> Z.to_N (n - m) = (Z.to_N n - Z.to_N m)%N
 destruct n as [|n|n], m as [|m|m]; trivial; try (now destruct 1).n, m:positive
0 <= Z.pos m ->
Z.to_N (Z.pos n - Z.pos m) =
(Z.to_N (Z.pos n) - Z.to_N (Z.pos m))%N
 intros _.n, m:positive
Z.to_N (Z.pos n - Z.pos m) =
(Z.to_N (Z.pos n) - Z.to_N (Z.pos m))%N simpl.n, m:positive
Z.to_N (Z.pos_sub n m) =
match Pos.sub_mask n m with
| Pos.IsPos p => N.pos p
| _ => 0%N
end
 rewrite Z.pos_sub_spec, Pos.compare_sub_mask.n, m:positive
Z.to_N
  match Pos.mask2cmp (Pos.sub_mask n m) with
  | Eq => 0
  | Lt => Z.neg (m - n)
  | Gt => Z.pos (n - m)
  end =
match Pos.sub_mask n m with
| Pos.IsPos p => N.pos p
| _ => 0%N
end unfold Pos.sub.n, m:positive
Z.to_N
  match Pos.mask2cmp (Pos.sub_mask n m) with
  | Eq => 0
  | Lt =>
      Z.neg
        match Pos.sub_mask m n with
        | Pos.IsPos z => z
        | _ => 1
        end
  | Gt =>
      Z.pos
        match Pos.sub_mask n m with
        | Pos.IsPos z => z
        | _ => 1
        end
  end =
match Pos.sub_mask n m with
| Pos.IsPos p => N.pos p
| _ => 0%N
end
 now destruct (Pos.sub_mask n m).
Qed.

Lemma inj_pred n : Z.to_N (Z.pred n) = N.pred (Z.to_N n).n:Z
Z.to_N (Z.pred n) = N.pred (Z.to_N n)
Proof.n:Z
Z.to_N (Z.pred n) = N.pred (Z.to_N n)
 unfold Z.pred.n:Z
Z.to_N (n + -1) = N.pred (Z.to_N n) rewrite <- N.sub_1_r.n:Z
Z.to_N (n + -1) = (Z.to_N n - 1)%N now apply (inj_sub n 1).
Qed.

Lemma inj_compare n m : 0<=n -> 0<=m ->
 (Z.to_N n ?= Z.to_N m)%N = (n ?= m).n, m:Z
0 <= n ->
0 <= m -> (Z.to_N n ?= Z.to_N m)%N = (n ?= m)
Proof.n, m:Z
0 <= n ->
0 <= m -> (Z.to_N n ?= Z.to_N m)%N = (n ?= m)
 intros Hn Hm.n, m:Z
Hn:0 <= n
Hm:0 <= m
(Z.to_N n ?= Z.to_N m)%N = (n ?= m) now rewrite <- N2Z.inj_compare, !id.
Qed.

Lemma inj_le n m : 0<=n -> 0<=m -> (n<=m <-> (Z.to_N n <= Z.to_N m)%N).n, m:Z
0 <= n ->
0 <= m -> n <= m <-> (Z.to_N n <= Z.to_N m)%N
Proof.n, m:Z
0 <= n ->
0 <= m -> n <= m <-> (Z.to_N n <= Z.to_N m)%N
 intros Hn Hm.n, m:Z
Hn:0 <= n
Hm:0 <= m
n <= m <-> (Z.to_N n <= Z.to_N m)%N unfold Z.le, N.le.n, m:Z
Hn:0 <= n
Hm:0 <= m
(n ?= m) <> Gt <-> (Z.to_N n ?= Z.to_N m)%N <> Gt now rewrite inj_compare.
Qed.

Lemma inj_lt n m : 0<=n -> 0<=m -> (n<m <-> (Z.to_N n < Z.to_N m)%N).n, m:Z
0 <= n -> 0 <= m -> n < m <-> (Z.to_N n < Z.to_N m)%N
Proof.n, m:Z
0 <= n -> 0 <= m -> n < m <-> (Z.to_N n < Z.to_N m)%N
 intros Hn Hm.n, m:Z
Hn:0 <= n
Hm:0 <= m
n < m <-> (Z.to_N n < Z.to_N m)%N unfold Z.lt, N.lt.n, m:Z
Hn:0 <= n
Hm:0 <= m
(n ?= m) = Lt <-> (Z.to_N n ?= Z.to_N m)%N = Lt now rewrite inj_compare.
Qed.

Lemma inj_min n m : Z.to_N (Z.min n m) = N.min (Z.to_N n) (Z.to_N m).n, m:Z
Z.to_N (Z.min n m) = N.min (Z.to_N n) (Z.to_N m)
Proof.n, m:Z
Z.to_N (Z.min n m) = N.min (Z.to_N n) (Z.to_N m)
 destruct n, m; simpl; trivial; unfold Z.min, N.min; simpl;
  now case Pos.compare.
Qed.

Lemma inj_max n m : Z.to_N (Z.max n m) = N.max (Z.to_N n) (Z.to_N m).n, m:Z
Z.to_N (Z.max n m) = N.max (Z.to_N n) (Z.to_N m)
Proof.n, m:Z
Z.to_N (Z.max n m) = N.max (Z.to_N n) (Z.to_N m)
 destruct n, m; simpl; trivial; unfold Z.max, N.max; simpl.p, p0:positive
Z.to_N
  match (p ?= p0)%positive with
  | Lt => Z.pos p0
  | _ => Z.pos p
  end =
match (p ?= p0)%positive with
| Gt => N.pos p
| _ => N.pos p0
end
p, p0:positive
Z.to_N
  match CompOpp (p ?= p0)%positive with
  | Lt => Z.neg p0
  | _ => Z.neg p
  end = 0%N
  case Pos.compare_spec; intros; subst; trivial.p, p0:positive
Z.to_N
  match CompOpp (p ?= p0)%positive with
  | Lt => Z.neg p0
  | _ => Z.neg p
  end = 0%N
  now case Pos.compare.
Qed.

Lemma inj_div n m : 0<=n -> 0<=m -> Z.to_N (n/m) = (Z.to_N n / Z.to_N m)%N.n, m:Z
0 <= n ->
0 <= m -> Z.to_N (n / m) = (Z.to_N n / Z.to_N m)%N
Proof.n, m:Z
0 <= n ->
0 <= m -> Z.to_N (n / m) = (Z.to_N n / Z.to_N m)%N
 destruct n, m; trivial; intros Hn Hm;
 (now destruct Hn) || (now destruct Hm) || clear.p, p0:positive
Z.to_N (Z.pos p / Z.pos p0) =
(Z.to_N (Z.pos p) / Z.to_N (Z.pos p0))%N
 simpl.p, p0:positive
Z.to_N (Z.pos p / Z.pos p0) = (N.pos p / N.pos p0)%N rewrite <- (N2Z.id (_ / _)).p, p0:positive
Z.to_N (Z.pos p / Z.pos p0) =
Z.to_N (Z.of_N (N.pos p / N.pos p0)) f_equal.p, p0:positive
Z.pos p / Z.pos p0 = Z.of_N (N.pos p / N.pos p0) now rewrite N2Z.inj_div.
Qed.

Lemma inj_mod n m : 0<=n -> 0<m ->
 Z.to_N (n mod m) = ((Z.to_N n) mod (Z.to_N m))%N.n, m:Z
0 <= n ->
0 < m -> Z.to_N (n mod m) = (Z.to_N n mod Z.to_N m)%N
Proof.n, m:Z
0 <= n ->
0 < m -> Z.to_N (n mod m) = (Z.to_N n mod Z.to_N m)%N
 destruct n, m; trivial; intros Hn Hm;
 (now destruct Hn) || (now destruct Hm) || clear.p, p0:positive
Z.to_N (Z.pos p mod Z.pos p0) =
(Z.to_N (Z.pos p) mod Z.to_N (Z.pos p0))%N
 simpl.p, p0:positive
Z.to_N (Z.pos p mod Z.pos p0) =
(N.pos p mod N.pos p0)%N rewrite <- (N2Z.id (_ mod _)).p, p0:positive
Z.to_N (Z.pos p mod Z.pos p0) =
Z.to_N (Z.of_N (N.pos p mod N.pos p0)) f_equal.p, p0:positive
Z.pos p mod Z.pos p0 = Z.of_N (N.pos p mod N.pos p0) now rewrite N2Z.inj_mod.
Qed.

Lemma inj_quot n m : 0<=n -> 0<=m -> Z.to_N (n÷m) = (Z.to_N n / Z.to_N m)%N.n, m:Z
0 <= n ->
0 <= m -> Z.to_N (n ÷ m) = (Z.to_N n / Z.to_N m)%N
Proof.n, m:Z
0 <= n ->
0 <= m -> Z.to_N (n ÷ m) = (Z.to_N n / Z.to_N m)%N
 destruct m.n:Z
0 <= n ->
0 <= 0 -> Z.to_N (n ÷ 0) = (Z.to_N n / Z.to_N 0)%N
n:Z
p:positive
0 <= n ->
0 <= Z.pos p ->
Z.to_N (n ÷ Z.pos p) = (Z.to_N n / Z.to_N (Z.pos p))%N
n:Z
p:positive
0 <= n ->
0 <= Z.neg p ->
Z.to_N (n ÷ Z.neg p) = (Z.to_N n / Z.to_N (Z.neg p))%N
 -n:Z
0 <= n ->
0 <= 0 -> Z.to_N (n ÷ 0) = (Z.to_N n / Z.to_N 0)%N now destruct n.
 -n:Z
p:positive
0 <= n ->
0 <= Z.pos p ->
Z.to_N (n ÷ Z.pos p) = (Z.to_N n / Z.to_N (Z.pos p))%N intros.n:Z
p:positive
H:0 <= n
H0:0 <= Z.pos p
Z.to_N (n ÷ Z.pos p) = (Z.to_N n / Z.to_N (Z.pos p))%N now rewrite Z.quot_div_nonneg, inj_div.
 -n:Z
p:positive
0 <= n ->
0 <= Z.neg p ->
Z.to_N (n ÷ Z.neg p) = (Z.to_N n / Z.to_N (Z.neg p))%N now destruct 2.
Qed.

Lemma inj_rem n m :0<=n -> 0<=m ->
 Z.to_N (Z.rem n m) = ((Z.to_N n) mod (Z.to_N m))%N.n, m:Z
0 <= n ->
0 <= m ->
Z.to_N (Z.rem n m) = (Z.to_N n mod Z.to_N m)%N
Proof.n, m:Z
0 <= n ->
0 <= m ->
Z.to_N (Z.rem n m) = (Z.to_N n mod Z.to_N m)%N
 destruct m.n:Z
0 <= n ->
0 <= 0 ->
Z.to_N (Z.rem n 0) = (Z.to_N n mod Z.to_N 0)%N
n:Z
p:positive
0 <= n ->
0 <= Z.pos p ->
Z.to_N (Z.rem n (Z.pos p)) =
(Z.to_N n mod Z.to_N (Z.pos p))%N
n:Z
p:positive
0 <= n ->
0 <= Z.neg p ->
Z.to_N (Z.rem n (Z.neg p)) =
(Z.to_N n mod Z.to_N (Z.neg p))%N
 -n:Z
0 <= n ->
0 <= 0 ->
Z.to_N (Z.rem n 0) = (Z.to_N n mod Z.to_N 0)%N now destruct n.
 -n:Z
p:positive
0 <= n ->
0 <= Z.pos p ->
Z.to_N (Z.rem n (Z.pos p)) =
(Z.to_N n mod Z.to_N (Z.pos p))%N intros.n:Z
p:positive
H:0 <= n
H0:0 <= Z.pos p
Z.to_N (Z.rem n (Z.pos p)) =
(Z.to_N n mod Z.to_N (Z.pos p))%N now rewrite Z.rem_mod_nonneg, inj_mod.
 -n:Z
p:positive
0 <= n ->
0 <= Z.neg p ->
Z.to_N (Z.rem n (Z.neg p)) =
(Z.to_N n mod Z.to_N (Z.neg p))%N now destruct 2.
Qed.

Lemma inj_div2 n : Z.to_N (Z.div2 n) = N.div2 (Z.to_N n).n:Z
Z.to_N (Z.div2 n) = N.div2 (Z.to_N n)
Proof.n:Z
Z.to_N (Z.div2 n) = N.div2 (Z.to_N n)
 destruct n as [|p|p]; trivial.p:positive
Z.to_N (Z.div2 (Z.pos p)) = N.div2 (Z.to_N (Z.pos p)) now destruct p.
Qed.

Lemma inj_quot2 n : Z.to_N (Z.quot2 n) = N.div2 (Z.to_N n).n:Z
Z.to_N (Z.quot2 n) = N.div2 (Z.to_N n)
Proof.n:Z
Z.to_N (Z.quot2 n) = N.div2 (Z.to_N n)
 destruct n as [|p|p]; trivial; now destruct p.
Qed.

Lemma inj_pow n m : 0<=n -> 0<=m -> Z.to_N (n^m) = ((Z.to_N n)^(Z.to_N m))%N.n, m:Z
0 <= n ->
0 <= m -> Z.to_N (n ^ m) = (Z.to_N n ^ Z.to_N m)%N
Proof.n, m:Z
0 <= n ->
0 <= m -> Z.to_N (n ^ m) = (Z.to_N n ^ Z.to_N m)%N
 destruct m.n:Z
0 <= n ->
0 <= 0 -> Z.to_N (n ^ 0) = (Z.to_N n ^ Z.to_N 0)%N
n:Z
p:positive
0 <= n ->
0 <= Z.pos p ->
Z.to_N (n ^ Z.pos p) = (Z.to_N n ^ Z.to_N (Z.pos p))%N
n:Z
p:positive
0 <= n ->
0 <= Z.neg p ->
Z.to_N (n ^ Z.neg p) = (Z.to_N n ^ Z.to_N (Z.neg p))%N
 -n:Z
0 <= n ->
0 <= 0 -> Z.to_N (n ^ 0) = (Z.to_N n ^ Z.to_N 0)%N trivial.
 -n:Z
p:positive
0 <= n ->
0 <= Z.pos p ->
Z.to_N (n ^ Z.pos p) = (Z.to_N n ^ Z.to_N (Z.pos p))%N intros.n:Z
p:positive
H:0 <= n
H0:0 <= Z.pos p
Z.to_N (n ^ Z.pos p) = (Z.to_N n ^ Z.to_N (Z.pos p))%N now rewrite <- (N2Z.id (_ ^ _)), N2Z.inj_pow, id.
 -n:Z
p:positive
0 <= n ->
0 <= Z.neg p ->
Z.to_N (n ^ Z.neg p) = (Z.to_N n ^ Z.to_N (Z.neg p))%N now destruct 2.
Qed.

Lemma inj_testbit a n : 0<=n ->
 Z.testbit (Z.of_N a) n = N.testbit a (Z.to_N n).a:N
n:Z
0 <= n ->
Z.testbit (Z.of_N a) n = N.testbit a (Z.to_N n)
Proof.a:N
n:Z
0 <= n ->
Z.testbit (Z.of_N a) n = N.testbit a (Z.to_N n) apply Z.testbit_of_N'. Qed.

End Z2N.

Module Zabs2N.

Results about Z.abs_N, converting absolute values of Z integers to N.

Lemma abs_N_spec n : Z.abs_N n = Z.to_N (Z.abs n).n:Z
Z.abs_N n = Z.to_N (Z.abs n)
Proof.n:Z
Z.abs_N n = Z.to_N (Z.abs n)
 now destruct n.
Qed.

Lemma abs_N_nonneg n : 0<=n -> Z.abs_N n = Z.to_N n.n:Z
0 <= n -> Z.abs_N n = Z.to_N n
Proof.n:Z
0 <= n -> Z.abs_N n = Z.to_N n
 destruct n; trivial; now destruct 1.
Qed.

Lemma id_abs n : Z.of_N (Z.abs_N n) = Z.abs n.n:Z
Z.of_N (Z.abs_N n) = Z.abs n
Proof.n:Z
Z.of_N (Z.abs_N n) = Z.abs n
 now destruct n.
Qed.

Lemma id n : Z.abs_N (Z.of_N n) = n.n:N
Z.abs_N (Z.of_N n) = n
Proof.n:N
Z.abs_N (Z.of_N n) = n
 now destruct n.
Qed.

Z.abs_N, basic equations

Lemma inj_0 : Z.abs_N 0 = 0%N.Z.abs_N 0 = 0%N
Proof.Z.abs_N 0 = 0%N
 reflexivity.
Qed.

Lemma inj_pos p : Z.abs_N (Zpos p) = Npos p.p:positive
Z.abs_N (Z.pos p) = N.pos p
Proof.p:positive
Z.abs_N (Z.pos p) = N.pos p
 reflexivity.
Qed.

Lemma inj_neg p : Z.abs_N (Zneg p) = Npos p.p:positive
Z.abs_N (Z.neg p) = N.pos p
Proof.p:positive
Z.abs_N (Z.neg p) = N.pos p
 reflexivity.
Qed.

Z.abs_N and usual operations, with non-negative integers

Lemma inj_opp n : Z.abs_N (-n) = Z.abs_N n.n:Z
Z.abs_N (- n) = Z.abs_N n
Proof.n:Z
Z.abs_N (- n) = Z.abs_N n
 now destruct n.
Qed.

Lemma inj_succ n : 0<=n -> Z.abs_N (Z.succ n) = N.succ (Z.abs_N n).n:Z
0 <= n -> Z.abs_N (Z.succ n) = N.succ (Z.abs_N n)
Proof.n:Z
0 <= n -> Z.abs_N (Z.succ n) = N.succ (Z.abs_N n)
 intros.n:Z
H:0 <= n
Z.abs_N (Z.succ n) = N.succ (Z.abs_N n) rewrite !abs_N_nonneg; trivial.n:Z
H:0 <= n
Z.to_N (Z.succ n) = N.succ (Z.to_N n)
n:Z
H:0 <= n
0 <= Z.succ n now apply Z2N.inj_succ.n:Z
H:0 <= n
0 <= Z.succ n
 now apply Z.le_le_succ_r.
Qed.

Lemma inj_add n m : 0<=n -> 0<=m -> Z.abs_N (n+m) = (Z.abs_N n + Z.abs_N m)%N.n, m:Z
0 <= n ->
0 <= m -> Z.abs_N (n + m) = (Z.abs_N n + Z.abs_N m)%N
Proof.n, m:Z
0 <= n ->
0 <= m -> Z.abs_N (n + m) = (Z.abs_N n + Z.abs_N m)%N
 intros.n, m:Z
H:0 <= n
H0:0 <= m
Z.abs_N (n + m) = (Z.abs_N n + Z.abs_N m)%N rewrite !abs_N_nonneg; trivial.n, m:Z
H:0 <= n
H0:0 <= m
Z.to_N (n + m) = (Z.to_N n + Z.to_N m)%N
n, m:Z
H:0 <= n
H0:0 <= m
0 <= n + m now apply Z2N.inj_add.n, m:Z
H:0 <= n
H0:0 <= m
0 <= n + m
 now apply Z.add_nonneg_nonneg.
Qed.

Lemma inj_mul n m : Z.abs_N (n*m) = (Z.abs_N n * Z.abs_N m)%N.n, m:Z
Z.abs_N (n * m) = (Z.abs_N n * Z.abs_N m)%N
Proof.n, m:Z
Z.abs_N (n * m) = (Z.abs_N n * Z.abs_N m)%N
 now destruct n, m.
Qed.

Lemma inj_sub n m : 0<=m<=n -> Z.abs_N (n-m) = (Z.abs_N n - Z.abs_N m)%N.n, m:Z
0 <= m <= n ->
Z.abs_N (n - m) = (Z.abs_N n - Z.abs_N m)%N
Proof.n, m:Z
0 <= m <= n ->
Z.abs_N (n - m) = (Z.abs_N n - Z.abs_N m)%N
 intros (Hn,H).n, m:Z
Hn:0 <= m
H:m <= n
Z.abs_N (n - m) = (Z.abs_N n - Z.abs_N m)%N rewrite !abs_N_nonneg; trivial.n, m:Z
Hn:0 <= m
H:m <= n
Z.to_N (n - m) = (Z.to_N n - Z.to_N m)%N
n, m:Z
Hn:0 <= m
H:m <= n
0 <= n
n, m:Z
Hn:0 <= m
H:m <= n
0 <= n - m now apply Z2N.inj_sub.n, m:Z
Hn:0 <= m
H:m <= n
0 <= n
n, m:Z
Hn:0 <= m
H:m <= n
0 <= n - m
 Z.order.n, m:Z
Hn:0 <= m
H:m <= n
0 <= n - m
 now apply Z.le_0_sub.
Qed.

Lemma inj_pred n : 0<n -> Z.abs_N (Z.pred n) = N.pred (Z.abs_N n).n:Z
0 < n -> Z.abs_N (Z.pred n) = N.pred (Z.abs_N n)
Proof.n:Z
0 < n -> Z.abs_N (Z.pred n) = N.pred (Z.abs_N n)
 intros.n:Z
H:0 < n
Z.abs_N (Z.pred n) = N.pred (Z.abs_N n) rewrite !abs_N_nonneg.n:Z
H:0 < n
Z.to_N (Z.pred n) = N.pred (Z.to_N n)
n:Z
H:0 < n
0 <= n
n:Z
H:0 < n
0 <= Z.pred n now apply Z2N.inj_pred.n:Z
H:0 < n
0 <= n
n:Z
H:0 < n
0 <= Z.pred n
 Z.order.n:Z
H:0 < n
0 <= Z.pred n
 apply Z.lt_succ_r.n:Z
H:0 < n
0 < Z.succ (Z.pred n) now rewrite Z.succ_pred.
Qed.

Lemma inj_compare n m : 0<=n -> 0<=m ->
 (Z.abs_N n ?= Z.abs_N m)%N = (n ?= m).n, m:Z
0 <= n ->
0 <= m -> (Z.abs_N n ?= Z.abs_N m)%N = (n ?= m)
Proof.n, m:Z
0 <= n ->
0 <= m -> (Z.abs_N n ?= Z.abs_N m)%N = (n ?= m)
 intros.n, m:Z
H:0 <= n
H0:0 <= m
(Z.abs_N n ?= Z.abs_N m)%N = (n ?= m) rewrite !abs_N_nonneg by trivial.n, m:Z
H:0 <= n
H0:0 <= m
(Z.to_N n ?= Z.to_N m)%N = (n ?= m) now apply Z2N.inj_compare.
Qed.

Lemma inj_le n m : 0<=n -> 0<=m -> (n<=m <-> (Z.abs_N n <= Z.abs_N m)%N).n, m:Z
0 <= n ->
0 <= m -> n <= m <-> (Z.abs_N n <= Z.abs_N m)%N
Proof.n, m:Z
0 <= n ->
0 <= m -> n <= m <-> (Z.abs_N n <= Z.abs_N m)%N
 intros Hn Hm.n, m:Z
Hn:0 <= n
Hm:0 <= m
n <= m <-> (Z.abs_N n <= Z.abs_N m)%N unfold Z.le, N.le.n, m:Z
Hn:0 <= n
Hm:0 <= m
(n ?= m) <> Gt <-> (Z.abs_N n ?= Z.abs_N m)%N <> Gt now rewrite inj_compare.
Qed.

Lemma inj_lt n m : 0<=n -> 0<=m -> (n<m <-> (Z.abs_N n < Z.abs_N m)%N).n, m:Z
0 <= n ->
0 <= m -> n < m <-> (Z.abs_N n < Z.abs_N m)%N
Proof.n, m:Z
0 <= n ->
0 <= m -> n < m <-> (Z.abs_N n < Z.abs_N m)%N
 intros Hn Hm.n, m:Z
Hn:0 <= n
Hm:0 <= m
n < m <-> (Z.abs_N n < Z.abs_N m)%N unfold Z.lt, N.lt.n, m:Z
Hn:0 <= n
Hm:0 <= m
(n ?= m) = Lt <-> (Z.abs_N n ?= Z.abs_N m)%N = Lt now rewrite inj_compare.
Qed.

Lemma inj_min n m : 0<=n -> 0<=m ->
 Z.abs_N (Z.min n m) = N.min (Z.abs_N n) (Z.abs_N m).n, m:Z
0 <= n ->
0 <= m ->
Z.abs_N (Z.min n m) = N.min (Z.abs_N n) (Z.abs_N m)
Proof.n, m:Z
0 <= n ->
0 <= m ->
Z.abs_N (Z.min n m) = N.min (Z.abs_N n) (Z.abs_N m)
 intros.n, m:Z
H:0 <= n
H0:0 <= m
Z.abs_N (Z.min n m) = N.min (Z.abs_N n) (Z.abs_N m) rewrite !abs_N_nonneg; trivial.n, m:Z
H:0 <= n
H0:0 <= m
Z.to_N (Z.min n m) = N.min (Z.to_N n) (Z.to_N m)
n, m:Z
H:0 <= n
H0:0 <= m
0 <= Z.min n m now apply Z2N.inj_min.n, m:Z
H:0 <= n
H0:0 <= m
0 <= Z.min n m
 now apply Z.min_glb.
Qed.

Lemma inj_max n m : 0<=n -> 0<=m ->
 Z.abs_N (Z.max n m) = N.max (Z.abs_N n) (Z.abs_N m).n, m:Z
0 <= n ->
0 <= m ->
Z.abs_N (Z.max n m) = N.max (Z.abs_N n) (Z.abs_N m)
Proof.n, m:Z
0 <= n ->
0 <= m ->
Z.abs_N (Z.max n m) = N.max (Z.abs_N n) (Z.abs_N m)
 intros.n, m:Z
H:0 <= n
H0:0 <= m
Z.abs_N (Z.max n m) = N.max (Z.abs_N n) (Z.abs_N m) rewrite !abs_N_nonneg; trivial.n, m:Z
H:0 <= n
H0:0 <= m
Z.to_N (Z.max n m) = N.max (Z.to_N n) (Z.to_N m)
n, m:Z
H:0 <= n
H0:0 <= m
0 <= Z.max n m now apply Z2N.inj_max.n, m:Z
H:0 <= n
H0:0 <= m
0 <= Z.max n m
 transitivity n; trivial.n, m:Z
H:0 <= n
H0:0 <= m
n <= Z.max n m apply Z.le_max_l.
Qed.

Lemma inj_quot n m : Z.abs_N (n÷m) = ((Z.abs_N n) / (Z.abs_N m))%N.n, m:Z
Z.abs_N (n ÷ m) = (Z.abs_N n / Z.abs_N m)%N
Proof.n, m:Z
Z.abs_N (n ÷ m) = (Z.abs_N n / Z.abs_N m)%N
 assert (forall p q, Z.abs_N (Zpos p ÷ Zpos q) = (Npos p / Npos q)%N).n, m:Z
forall p q : positive,
Z.abs_N (Z.pos p ÷ Z.pos q) = (N.pos p / N.pos q)%N
n, m:Z
H:forall p q : positive,
Z.abs_N (Z.pos p ÷ Z.pos q) =
(N.pos p / N.pos q)%N
Z.abs_N (n ÷ m) = (Z.abs_N n / Z.abs_N m)%N
  intros.n, m:Z
p, q:positive
Z.abs_N (Z.pos p ÷ Z.pos q) = (N.pos p / N.pos q)%N
n, m:Z
H:forall p q : positive,
Z.abs_N (Z.pos p ÷ Z.pos q) =
(N.pos p / N.pos q)%N
Z.abs_N (n ÷ m) = (Z.abs_N n / Z.abs_N m)%N rewrite abs_N_nonneg.n, m:Z
p, q:positive
Z.to_N (Z.pos p ÷ Z.pos q) = (N.pos p / N.pos q)%N
n, m:Z
p, q:positive
0 <= Z.pos p ÷ Z.pos q
n, m:Z
H:forall p q : positive,
Z.abs_N (Z.pos p ÷ Z.pos q) =
(N.pos p / N.pos q)%N
Z.abs_N (n ÷ m) = (Z.abs_N n / Z.abs_N m)%N now apply Z2N.inj_quot.n, m:Z
p, q:positive
0 <= Z.pos p ÷ Z.pos q
n, m:Z
H:forall p q : positive,
Z.abs_N (Z.pos p ÷ Z.pos q) =
(N.pos p / N.pos q)%N
Z.abs_N (n ÷ m) = (Z.abs_N n / Z.abs_N m)%N now apply Z.quot_pos.n, m:Z
H:forall p q : positive,
Z.abs_N (Z.pos p ÷ Z.pos q) =
(N.pos p / N.pos q)%N
Z.abs_N (n ÷ m) = (Z.abs_N n / Z.abs_N m)%N
 destruct n, m; trivial; simpl.p, p0:positive
H:forall p1 q : positive,
Z.abs_N (Z.pos p1 ÷ Z.pos q) =
(N.pos p1 / N.pos q)%N
Z.abs_N (Z.pos p ÷ Z.pos p0) = (N.pos p / N.pos p0)%N
p, p0:positive
H:forall p1 q : positive,
Z.abs_N (Z.pos p1 ÷ Z.pos q) =
(N.pos p1 / N.pos q)%N
Z.abs_N (Z.pos p ÷ Z.neg p0) = (N.pos p / N.pos p0)%N
p, p0:positive
H:forall p1 q : positive,
Z.abs_N (Z.pos p1 ÷ Z.pos q) =
(N.pos p1 / N.pos q)%N
Z.abs_N (Z.neg p ÷ Z.pos p0) = (N.pos p / N.pos p0)%N
p, p0:positive
H:forall p1 q : positive,
Z.abs_N (Z.pos p1 ÷ Z.pos q) =
(N.pos p1 / N.pos q)%N
Z.abs_N (Z.neg p ÷ Z.neg p0) = (N.pos p / N.pos p0)%N
 -p, p0:positive
H:forall p1 q : positive,
Z.abs_N (Z.pos p1 ÷ Z.pos q) =
(N.pos p1 / N.pos q)%N
Z.abs_N (Z.pos p ÷ Z.pos p0) = (N.pos p / N.pos p0)%N trivial.
 -p, p0:positive
H:forall p1 q : positive,
Z.abs_N (Z.pos p1 ÷ Z.pos q) =
(N.pos p1 / N.pos q)%N
Z.abs_N (Z.pos p ÷ Z.neg p0) = (N.pos p / N.pos p0)%N now rewrite <- Pos2Z.opp_pos, Z.quot_opp_r, inj_opp.
 -p, p0:positive
H:forall p1 q : positive,
Z.abs_N (Z.pos p1 ÷ Z.pos q) =
(N.pos p1 / N.pos q)%N
Z.abs_N (Z.neg p ÷ Z.pos p0) = (N.pos p / N.pos p0)%N now rewrite <- Pos2Z.opp_pos, Z.quot_opp_l, inj_opp.
 -p, p0:positive
H:forall p1 q : positive,
Z.abs_N (Z.pos p1 ÷ Z.pos q) =
(N.pos p1 / N.pos q)%N
Z.abs_N (Z.neg p ÷ Z.neg p0) = (N.pos p / N.pos p0)%N now rewrite <- 2 Pos2Z.opp_pos, Z.quot_opp_opp.
Qed.

Lemma inj_rem n m : Z.abs_N (Z.rem n m) = ((Z.abs_N n) mod (Z.abs_N m))%N.n, m:Z
Z.abs_N (Z.rem n m) = (Z.abs_N n mod Z.abs_N m)%N
Proof.n, m:Z
Z.abs_N (Z.rem n m) = (Z.abs_N n mod Z.abs_N m)%N
 assert
  (forall p q, Z.abs_N (Z.rem (Zpos p) (Zpos q)) = ((Npos p) mod (Npos q))%N).n, m:Z
forall p q : positive,
Z.abs_N (Z.rem (Z.pos p) (Z.pos q)) =
(N.pos p mod N.pos q)%N
n, m:Z
H:forall p q : positive,
Z.abs_N (Z.rem (Z.pos p) (Z.pos q)) =
(N.pos p mod N.pos q)%N
Z.abs_N (Z.rem n m) = (Z.abs_N n mod Z.abs_N m)%N
  intros.n, m:Z
p, q:positive
Z.abs_N (Z.rem (Z.pos p) (Z.pos q)) =
(N.pos p mod N.pos q)%N
n, m:Z
H:forall p q : positive,
Z.abs_N (Z.rem (Z.pos p) (Z.pos q)) =
(N.pos p mod N.pos q)%N
Z.abs_N (Z.rem n m) = (Z.abs_N n mod Z.abs_N m)%N rewrite abs_N_nonneg.n, m:Z
p, q:positive
Z.to_N (Z.rem (Z.pos p) (Z.pos q)) =
(N.pos p mod N.pos q)%N
n, m:Z
p, q:positive
0 <= Z.rem (Z.pos p) (Z.pos q)
n, m:Z
H:forall p q : positive,
Z.abs_N (Z.rem (Z.pos p) (Z.pos q)) =
(N.pos p mod N.pos q)%N
Z.abs_N (Z.rem n m) = (Z.abs_N n mod Z.abs_N m)%N now apply Z2N.inj_rem.n, m:Z
p, q:positive
0 <= Z.rem (Z.pos p) (Z.pos q)
n, m:Z
H:forall p q : positive,
Z.abs_N (Z.rem (Z.pos p) (Z.pos q)) =
(N.pos p mod N.pos q)%N
Z.abs_N (Z.rem n m) = (Z.abs_N n mod Z.abs_N m)%N now apply Z.rem_nonneg.n, m:Z
H:forall p q : positive,
Z.abs_N (Z.rem (Z.pos p) (Z.pos q)) =
(N.pos p mod N.pos q)%N
Z.abs_N (Z.rem n m) = (Z.abs_N n mod Z.abs_N m)%N
 destruct n, m; trivial; simpl.p, p0:positive
H:forall p1 q : positive,
Z.abs_N (Z.rem (Z.pos p1) (Z.pos q)) =
(N.pos p1 mod N.pos q)%N
Z.abs_N (Z.rem (Z.pos p) (Z.pos p0)) =
(N.pos p mod N.pos p0)%N
p, p0:positive
H:forall p1 q : positive,
Z.abs_N (Z.rem (Z.pos p1) (Z.pos q)) =
(N.pos p1 mod N.pos q)%N
Z.abs_N (Z.rem (Z.pos p) (Z.neg p0)) =
(N.pos p mod N.pos p0)%N
p, p0:positive
H:forall p1 q : positive,
Z.abs_N (Z.rem (Z.pos p1) (Z.pos q)) =
(N.pos p1 mod N.pos q)%N
Z.abs_N (Z.rem (Z.neg p) (Z.pos p0)) =
(N.pos p mod N.pos p0)%N
p, p0:positive
H:forall p1 q : positive,
Z.abs_N (Z.rem (Z.pos p1) (Z.pos q)) =
(N.pos p1 mod N.pos q)%N
Z.abs_N (Z.rem (Z.neg p) (Z.neg p0)) =
(N.pos p mod N.pos p0)%N
 -p, p0:positive
H:forall p1 q : positive,
Z.abs_N (Z.rem (Z.pos p1) (Z.pos q)) =
(N.pos p1 mod N.pos q)%N
Z.abs_N (Z.rem (Z.pos p) (Z.pos p0)) =
(N.pos p mod N.pos p0)%N trivial.
 -p, p0:positive
H:forall p1 q : positive,
Z.abs_N (Z.rem (Z.pos p1) (Z.pos q)) =
(N.pos p1 mod N.pos q)%N
Z.abs_N (Z.rem (Z.pos p) (Z.neg p0)) =
(N.pos p mod N.pos p0)%N now rewrite <- Pos2Z.opp_pos, Z.rem_opp_r.
 -p, p0:positive
H:forall p1 q : positive,
Z.abs_N (Z.rem (Z.pos p1) (Z.pos q)) =
(N.pos p1 mod N.pos q)%N
Z.abs_N (Z.rem (Z.neg p) (Z.pos p0)) =
(N.pos p mod N.pos p0)%N now rewrite <- Pos2Z.opp_pos, Z.rem_opp_l, inj_opp.
 -p, p0:positive
H:forall p1 q : positive,
Z.abs_N (Z.rem (Z.pos p1) (Z.pos q)) =
(N.pos p1 mod N.pos q)%N
Z.abs_N (Z.rem (Z.neg p) (Z.neg p0)) =
(N.pos p mod N.pos p0)%N now rewrite <- 2 Pos2Z.opp_pos, Z.rem_opp_opp, inj_opp.
Qed.

Lemma inj_pow n m : 0<=m -> Z.abs_N (n^m) = ((Z.abs_N n)^(Z.abs_N m))%N.n, m:Z
0 <= m -> Z.abs_N (n ^ m) = (Z.abs_N n ^ Z.abs_N m)%N
Proof.n, m:Z
0 <= m -> Z.abs_N (n ^ m) = (Z.abs_N n ^ Z.abs_N m)%N
 intros Hm.n, m:Z
Hm:0 <= m
Z.abs_N (n ^ m) = (Z.abs_N n ^ Z.abs_N m)%N rewrite abs_N_spec, Z.abs_pow, Z2N.inj_pow, <- abs_N_spec; trivial.n, m:Z
Hm:0 <= m
(Z.abs_N n ^ Z.to_N m)%N = (Z.abs_N n ^ Z.abs_N m)%N
n, m:Z
Hm:0 <= m
0 <= Z.abs n
 f_equal.n, m:Z
Hm:0 <= m
Z.to_N m = Z.abs_N m
n, m:Z
Hm:0 <= m
0 <= Z.abs n symmetry; now apply abs_N_nonneg.n, m:Z
Hm:0 <= m
0 <= Z.abs n apply Z.abs_nonneg.
Qed.

Z.abs_N and usual operations, statements with Z.abs

Lemma inj_succ_abs n : Z.abs_N (Z.succ (Z.abs n)) = N.succ (Z.abs_N n).n:Z
Z.abs_N (Z.succ (Z.abs n)) = N.succ (Z.abs_N n)
Proof.n:Z
Z.abs_N (Z.succ (Z.abs n)) = N.succ (Z.abs_N n)
 destruct n; simpl; trivial; now rewrite Pos.add_1_r.
Qed.

Lemma inj_add_abs n m :
 Z.abs_N (Z.abs n + Z.abs m) = (Z.abs_N n + Z.abs_N m)%N.n, m:Z
Z.abs_N (Z.abs n + Z.abs m) =
(Z.abs_N n + Z.abs_N m)%N
Proof.n, m:Z
Z.abs_N (Z.abs n + Z.abs m) =
(Z.abs_N n + Z.abs_N m)%N
 now destruct n, m.
Qed.

Lemma inj_mul_abs n m :
 Z.abs_N (Z.abs n * Z.abs m) = (Z.abs_N n * Z.abs_N m)%N.n, m:Z
Z.abs_N (Z.abs n * Z.abs m) =
(Z.abs_N n * Z.abs_N m)%N
Proof.n, m:Z
Z.abs_N (Z.abs n * Z.abs m) =
(Z.abs_N n * Z.abs_N m)%N
 now destruct n, m.
Qed.

End Zabs2N.

Conversions between Z and nat

Module Nat2Z.

Z.of_nat, basic equations

Lemma inj_0 : Z.of_nat 0 = 0.Z.of_nat 0 = 0
Proof.Z.of_nat 0 = 0
 reflexivity.
Qed.

Lemma inj_succ n : Z.of_nat (S n) = Z.succ (Z.of_nat n).n:nat
Z.of_nat (S n) = Z.succ (Z.of_nat n)
Proof.n:nat
Z.of_nat (S n) = Z.succ (Z.of_nat n)
 destruct n.Z.of_nat 1 = Z.succ (Z.of_nat 0)
n:nat
Z.of_nat (S (S n)) = Z.succ (Z.of_nat (S n)) trivial.n:nat
Z.of_nat (S (S n)) = Z.succ (Z.of_nat (S n)) simpl.n:nat
Z.pos (Pos.succ (Pos.of_succ_nat n)) =
Z.pos (Pos.of_succ_nat n + 1) apply Pos2Z.inj_succ.
Qed.

Register inj_succ as num.Nat2Z.inj_succ.

Z.of_N produce non-negative integers

Lemma is_nonneg n : 0 <= Z.of_nat n.n:nat
0 <= Z.of_nat n
Proof.n:nat
0 <= Z.of_nat n
 now induction n.
Qed.

Z.of_nat is a bijection between nat and non-negative Z, with Z.to_nat (or Z.abs_nat) as reciprocal. See Z2Nat.id below for the dual equation.

Lemma id n : Z.to_nat (Z.of_nat n) = n.n:nat
Z.to_nat (Z.of_nat n) = n
Proof.n:nat
Z.to_nat (Z.of_nat n) = n
 now rewrite <- nat_N_Z, <- Z_N_nat, N2Z.id, Nat2N.id.
Qed.

Z.of_nat is hence injective

Lemma inj n m : Z.of_nat n = Z.of_nat m -> n = m.n, m:nat
Z.of_nat n = Z.of_nat m -> n = m
Proof.n, m:nat
Z.of_nat n = Z.of_nat m -> n = m
 intros H.n, m:nat
H:Z.of_nat n = Z.of_nat m
n = m now rewrite <- (id n), <- (id m), H.
Qed.

Lemma inj_iff n m : Z.of_nat n = Z.of_nat m <-> n = m.n, m:nat
Z.of_nat n = Z.of_nat m <-> n = m
Proof.n, m:nat
Z.of_nat n = Z.of_nat m <-> n = m
 split.n, m:nat
Z.of_nat n = Z.of_nat m -> n = m
n, m:nat
n = m -> Z.of_nat n = Z.of_nat m apply inj.n, m:nat
n = m -> Z.of_nat n = Z.of_nat m intros; now f_equal.
Qed.

Z.of_nat and usual operations

Lemma inj_compare n m : (Z.of_nat n ?= Z.of_nat m) = (n ?= m)%nat.n, m:nat
(Z.of_nat n ?= Z.of_nat m) = (n ?= m)%nat
Proof.n, m:nat
(Z.of_nat n ?= Z.of_nat m) = (n ?= m)%nat
 now rewrite <-!nat_N_Z, N2Z.inj_compare, <- Nat2N.inj_compare.
Qed.

Lemma inj_le n m : (n<=m)%nat <-> Z.of_nat n <= Z.of_nat m.n, m:nat
(n <= m)%nat <-> Z.of_nat n <= Z.of_nat m
Proof.n, m:nat
(n <= m)%nat <-> Z.of_nat n <= Z.of_nat m
 unfold Z.le.n, m:nat
(n <= m)%nat <-> (Z.of_nat n ?= Z.of_nat m) <> Gt now rewrite inj_compare, nat_compare_le.
Qed.

Lemma inj_lt n m : (n<m)%nat <-> Z.of_nat n < Z.of_nat m.n, m:nat
(n < m)%nat <-> Z.of_nat n < Z.of_nat m
Proof.n, m:nat
(n < m)%nat <-> Z.of_nat n < Z.of_nat m
 unfold Z.lt.n, m:nat
(n < m)%nat <-> (Z.of_nat n ?= Z.of_nat m) = Lt now rewrite inj_compare, nat_compare_lt.
Qed.

Lemma inj_ge n m : (n>=m)%nat <-> Z.of_nat n >= Z.of_nat m.n, m:nat
(n >= m)%nat <-> Z.of_nat n >= Z.of_nat m
Proof.n, m:nat
(n >= m)%nat <-> Z.of_nat n >= Z.of_nat m
 unfold Z.ge.n, m:nat
(n >= m)%nat <-> (Z.of_nat n ?= Z.of_nat m) <> Lt now rewrite inj_compare, nat_compare_ge.
Qed.

Lemma inj_gt n m : (n>m)%nat <-> Z.of_nat n > Z.of_nat m.n, m:nat
(n > m)%nat <-> Z.of_nat n > Z.of_nat m
Proof.n, m:nat
(n > m)%nat <-> Z.of_nat n > Z.of_nat m
 unfold Z.gt.n, m:nat
(n > m)%nat <-> (Z.of_nat n ?= Z.of_nat m) = Gt now rewrite inj_compare, nat_compare_gt.
Qed.

Lemma inj_abs_nat z : Z.of_nat (Z.abs_nat z) = Z.abs z.z:Z
Z.of_nat (Z.abs_nat z) = Z.abs z
Proof.z:Z
Z.of_nat (Z.abs_nat z) = Z.abs z
 destruct z; simpl; trivial;
  destruct (Pos2Nat.is_succ p) as (n,H); rewrite H; simpl; f_equal;
   now apply SuccNat2Pos.inv.
Qed.

Lemma inj_add n m : Z.of_nat (n+m) = Z.of_nat n + Z.of_nat m.n, m:nat
Z.of_nat (n + m) = Z.of_nat n + Z.of_nat m
Proof.n, m:nat
Z.of_nat (n + m) = Z.of_nat n + Z.of_nat m
 now rewrite <- !nat_N_Z, Nat2N.inj_add, N2Z.inj_add.
Qed.

Register inj_add as num.Nat2Z.inj_add.

Lemma inj_mul n m : Z.of_nat (n*m) = Z.of_nat n * Z.of_nat m.n, m:nat
Z.of_nat (n * m) = Z.of_nat n * Z.of_nat m
Proof.n, m:nat
Z.of_nat (n * m) = Z.of_nat n * Z.of_nat m
 now rewrite <- !nat_N_Z, Nat2N.inj_mul, N2Z.inj_mul.
Qed.

Register inj_mul as num.Nat2Z.inj_mul.

Lemma inj_sub_max n m : Z.of_nat (n-m) = Z.max 0 (Z.of_nat n - Z.of_nat m).n, m:nat
Z.of_nat (n - m) = Z.max 0 (Z.of_nat n - Z.of_nat m)
Proof.n, m:nat
Z.of_nat (n - m) = Z.max 0 (Z.of_nat n - Z.of_nat m)
 now rewrite <- !nat_N_Z, Nat2N.inj_sub, N2Z.inj_sub_max.
Qed.

Lemma inj_sub n m : (m<=n)%nat -> Z.of_nat (n-m) = Z.of_nat n - Z.of_nat m.n, m:nat
(m <= n)%nat ->
Z.of_nat (n - m) = Z.of_nat n - Z.of_nat m
Proof.n, m:nat
(m <= n)%nat ->
Z.of_nat (n - m) = Z.of_nat n - Z.of_nat m
 rewrite nat_compare_le, Nat2N.inj_compare.n, m:nat
(N.of_nat m ?= N.of_nat n)%N <> Gt ->
Z.of_nat (n - m) = Z.of_nat n - Z.of_nat m intros.n, m:nat
H:(N.of_nat m ?= N.of_nat n)%N <> Gt
Z.of_nat (n - m) = Z.of_nat n - Z.of_nat m
 now rewrite <- !nat_N_Z, Nat2N.inj_sub, N2Z.inj_sub.
Qed.

Register inj_sub as num.Nat2Z.inj_sub.

Lemma inj_pred_max n : Z.of_nat (Nat.pred n) = Z.max 0 (Z.pred (Z.of_nat n)).n:nat
Z.of_nat (Nat.pred n) = Z.max 0 (Z.pred (Z.of_nat n))
Proof.n:nat
Z.of_nat (Nat.pred n) = Z.max 0 (Z.pred (Z.of_nat n))
 now rewrite <- !nat_N_Z, Nat2N.inj_pred, N2Z.inj_pred_max.
Qed.

Lemma inj_pred n : (0<n)%nat -> Z.of_nat (Nat.pred n) = Z.pred (Z.of_nat n).n:nat
(0 < n)%nat ->
Z.of_nat (Nat.pred n) = Z.pred (Z.of_nat n)
Proof.n:nat
(0 < n)%nat ->
Z.of_nat (Nat.pred n) = Z.pred (Z.of_nat n)
 rewrite nat_compare_lt, Nat2N.inj_compare.n:nat
(N.of_nat 0 ?= N.of_nat n)%N = Lt ->
Z.of_nat (Nat.pred n) = Z.pred (Z.of_nat n) intros.n:nat
H:(N.of_nat 0 ?= N.of_nat n)%N = Lt
Z.of_nat (Nat.pred n) = Z.pred (Z.of_nat n)
 now rewrite <- !nat_N_Z, Nat2N.inj_pred, N2Z.inj_pred.
Qed.

Lemma inj_min n m : Z.of_nat (Nat.min n m) = Z.min (Z.of_nat n) (Z.of_nat m).n, m:nat
Z.of_nat (Nat.min n m) =
Z.min (Z.of_nat n) (Z.of_nat m)
Proof.n, m:nat
Z.of_nat (Nat.min n m) =
Z.min (Z.of_nat n) (Z.of_nat m)
 now rewrite <- !nat_N_Z, Nat2N.inj_min, N2Z.inj_min.
Qed.

Lemma inj_max n m : Z.of_nat (Nat.max n m) = Z.max (Z.of_nat n) (Z.of_nat m).n, m:nat
Z.of_nat (Nat.max n m) =
Z.max (Z.of_nat n) (Z.of_nat m)
Proof.n, m:nat
Z.of_nat (Nat.max n m) =
Z.max (Z.of_nat n) (Z.of_nat m)
 now rewrite <- !nat_N_Z, Nat2N.inj_max, N2Z.inj_max.
Qed.

End Nat2Z.

Module Z2Nat.

Z.to_nat is a bijection between non-negative Z and nat, with Pos.of_nat as reciprocal. See nat2Z.id above for the dual equation.

Lemma id n : 0<=n -> Z.of_nat (Z.to_nat n) = n.n:Z
0 <= n -> Z.of_nat (Z.to_nat n) = n
Proof.n:Z
0 <= n -> Z.of_nat (Z.to_nat n) = n
 intros.n:Z
H:0 <= n
Z.of_nat (Z.to_nat n) = n now rewrite <- Z_N_nat, <- nat_N_Z, N2Nat.id, Z2N.id.
Qed.

Z.to_nat is hence injective for non-negative integers.

Lemma inj n m : 0<=n -> 0<=m -> Z.to_nat n = Z.to_nat m -> n = m.n, m:Z
0 <= n -> 0 <= m -> Z.to_nat n = Z.to_nat m -> n = m
Proof.n, m:Z
0 <= n -> 0 <= m -> Z.to_nat n = Z.to_nat m -> n = m
 intros.n, m:Z
H:0 <= n
H0:0 <= m
H1:Z.to_nat n = Z.to_nat m
n = m rewrite <- (id n), <- (id m) by trivial.n, m:Z
H:0 <= n
H0:0 <= m
H1:Z.to_nat n = Z.to_nat m
Z.of_nat (Z.to_nat n) = Z.of_nat (Z.to_nat m) now f_equal.
Qed.

Lemma inj_iff n m : 0<=n -> 0<=m -> (Z.to_nat n = Z.to_nat m <-> n = m).n, m:Z
0 <= n -> 0 <= m -> Z.to_nat n = Z.to_nat m <-> n = m
Proof.n, m:Z
0 <= n -> 0 <= m -> Z.to_nat n = Z.to_nat m <-> n = m
 intros.n, m:Z
H:0 <= n
H0:0 <= m
Z.to_nat n = Z.to_nat m <-> n = m split.n, m:Z
H:0 <= n
H0:0 <= m
Z.to_nat n = Z.to_nat m -> n = m
n, m:Z
H:0 <= n
H0:0 <= m
n = m -> Z.to_nat n = Z.to_nat m now apply inj.n, m:Z
H:0 <= n
H0:0 <= m
n = m -> Z.to_nat n = Z.to_nat m intros; now subst.
Qed.

Z.to_nat, basic equations

Lemma inj_0 : Z.to_nat 0 = O.Z.to_nat 0 = 0%nat
Proof.Z.to_nat 0 = 0%nat
 reflexivity.
Qed.

Lemma inj_pos n : Z.to_nat (Zpos n) = Pos.to_nat n.n:positive
Z.to_nat (Z.pos n) = Pos.to_nat n
Proof.n:positive
Z.to_nat (Z.pos n) = Pos.to_nat n
 reflexivity.
Qed.

Lemma inj_neg n : Z.to_nat (Zneg n) = O.n:positive
Z.to_nat (Z.neg n) = 0%nat
Proof.n:positive
Z.to_nat (Z.neg n) = 0%nat
 reflexivity.
Qed.

Z.to_nat and operations

Lemma inj_add n m : 0<=n -> 0<=m ->
 Z.to_nat (n+m) = (Z.to_nat n + Z.to_nat m)%nat.n, m:Z
0 <= n ->
0 <= m ->
Z.to_nat (n + m) = (Z.to_nat n + Z.to_nat m)%nat
Proof.n, m:Z
0 <= n ->
0 <= m ->
Z.to_nat (n + m) = (Z.to_nat n + Z.to_nat m)%nat
 intros.n, m:Z
H:0 <= n
H0:0 <= m
Z.to_nat (n + m) = (Z.to_nat n + Z.to_nat m)%nat now rewrite <- !Z_N_nat, Z2N.inj_add, N2Nat.inj_add.
Qed.

Lemma inj_mul n m : 0<=n -> 0<=m ->
 Z.to_nat (n*m) = (Z.to_nat n * Z.to_nat m)%nat.n, m:Z
0 <= n ->
0 <= m ->
Z.to_nat (n * m) = (Z.to_nat n * Z.to_nat m)%nat
Proof.n, m:Z
0 <= n ->
0 <= m ->
Z.to_nat (n * m) = (Z.to_nat n * Z.to_nat m)%nat
 intros.n, m:Z
H:0 <= n
H0:0 <= m
Z.to_nat (n * m) = (Z.to_nat n * Z.to_nat m)%nat now rewrite <- !Z_N_nat, Z2N.inj_mul, N2Nat.inj_mul.
Qed.

Lemma inj_succ n : 0<=n -> Z.to_nat (Z.succ n) = S (Z.to_nat n).n:Z
0 <= n -> Z.to_nat (Z.succ n) = S (Z.to_nat n)
Proof.n:Z
0 <= n -> Z.to_nat (Z.succ n) = S (Z.to_nat n)
 intros.n:Z
H:0 <= n
Z.to_nat (Z.succ n) = S (Z.to_nat n) now rewrite <- !Z_N_nat, Z2N.inj_succ, N2Nat.inj_succ.
Qed.

Lemma inj_sub n m : 0<=m -> Z.to_nat (n - m) = (Z.to_nat n - Z.to_nat m)%nat.n, m:Z
0 <= m ->
Z.to_nat (n - m) = (Z.to_nat n - Z.to_nat m)%nat
Proof.n, m:Z
0 <= m ->
Z.to_nat (n - m) = (Z.to_nat n - Z.to_nat m)%nat
 intros.n, m:Z
H:0 <= m
Z.to_nat (n - m) = (Z.to_nat n - Z.to_nat m)%nat now rewrite <- !Z_N_nat, Z2N.inj_sub, N2Nat.inj_sub.
Qed.

Lemma inj_pred n : Z.to_nat (Z.pred n) = Nat.pred (Z.to_nat n).n:Z
Z.to_nat (Z.pred n) = Nat.pred (Z.to_nat n)
Proof.n:Z
Z.to_nat (Z.pred n) = Nat.pred (Z.to_nat n)
 now rewrite <- !Z_N_nat, Z2N.inj_pred, N2Nat.inj_pred.
Qed.

Lemma inj_compare n m : 0<=n -> 0<=m ->
 (Z.to_nat n ?= Z.to_nat m)%nat = (n ?= m).n, m:Z
0 <= n ->
0 <= m -> (Z.to_nat n ?= Z.to_nat m)%nat = (n ?= m)
Proof.n, m:Z
0 <= n ->
0 <= m -> (Z.to_nat n ?= Z.to_nat m)%nat = (n ?= m)
 intros Hn Hm.n, m:Z
Hn:0 <= n
Hm:0 <= m
(Z.to_nat n ?= Z.to_nat m)%nat = (n ?= m) now rewrite <- Nat2Z.inj_compare, !id.
Qed.

Lemma inj_le n m : 0<=n -> 0<=m -> (n<=m <-> (Z.to_nat n <= Z.to_nat m)%nat).n, m:Z
0 <= n ->
0 <= m -> n <= m <-> (Z.to_nat n <= Z.to_nat m)%nat
Proof.n, m:Z
0 <= n ->
0 <= m -> n <= m <-> (Z.to_nat n <= Z.to_nat m)%nat
 intros Hn Hm.n, m:Z
Hn:0 <= n
Hm:0 <= m
n <= m <-> (Z.to_nat n <= Z.to_nat m)%nat unfold Z.le.n, m:Z
Hn:0 <= n
Hm:0 <= m
(n ?= m) <> Gt <-> (Z.to_nat n <= Z.to_nat m)%nat now rewrite nat_compare_le, inj_compare.
Qed.

Lemma inj_lt n m : 0<=n -> 0<=m -> (n<m <-> (Z.to_nat n < Z.to_nat m)%nat).n, m:Z
0 <= n ->
0 <= m -> n < m <-> (Z.to_nat n < Z.to_nat m)%nat
Proof.n, m:Z
0 <= n ->
0 <= m -> n < m <-> (Z.to_nat n < Z.to_nat m)%nat
 intros Hn Hm.n, m:Z
Hn:0 <= n
Hm:0 <= m
n < m <-> (Z.to_nat n < Z.to_nat m)%nat unfold Z.lt.n, m:Z
Hn:0 <= n
Hm:0 <= m
(n ?= m) = Lt <-> (Z.to_nat n < Z.to_nat m)%nat now rewrite nat_compare_lt, inj_compare.
Qed.

Lemma inj_min n m : Z.to_nat (Z.min n m) = Nat.min (Z.to_nat n) (Z.to_nat m).n, m:Z
Z.to_nat (Z.min n m) =
Nat.min (Z.to_nat n) (Z.to_nat m)
Proof.n, m:Z
Z.to_nat (Z.min n m) =
Nat.min (Z.to_nat n) (Z.to_nat m)
 now rewrite <- !Z_N_nat, Z2N.inj_min, N2Nat.inj_min.
Qed.

Lemma inj_max n m : Z.to_nat (Z.max n m) = Nat.max (Z.to_nat n) (Z.to_nat m).n, m:Z
Z.to_nat (Z.max n m) =
Nat.max (Z.to_nat n) (Z.to_nat m)
Proof.n, m:Z
Z.to_nat (Z.max n m) =
Nat.max (Z.to_nat n) (Z.to_nat m)
 now rewrite <- !Z_N_nat, Z2N.inj_max, N2Nat.inj_max.
Qed.

End Z2Nat.

Module Zabs2Nat.

Results about Z.abs_nat, converting absolute values of Z integers to nat.

Lemma abs_nat_spec n : Z.abs_nat n = Z.to_nat (Z.abs n).n:Z
Z.abs_nat n = Z.to_nat (Z.abs n)
Proof.n:Z
Z.abs_nat n = Z.to_nat (Z.abs n)
 now destruct n.
Qed.

Lemma abs_nat_nonneg n : 0<=n -> Z.abs_nat n = Z.to_nat n.n:Z
0 <= n -> Z.abs_nat n = Z.to_nat n
Proof.n:Z
0 <= n -> Z.abs_nat n = Z.to_nat n
 destruct n; trivial; now destruct 1.
Qed.

Lemma id_abs n : Z.of_nat (Z.abs_nat n) = Z.abs n.n:Z
Z.of_nat (Z.abs_nat n) = Z.abs n
Proof.n:Z
Z.of_nat (Z.abs_nat n) = Z.abs n
 rewrite <-Zabs_N_nat, N_nat_Z.n:Z
Z.of_N (Z.abs_N n) = Z.abs n apply Zabs2N.id_abs.
Qed.

Lemma id n : Z.abs_nat (Z.of_nat n) = n.n:nat
Z.abs_nat (Z.of_nat n) = n
Proof.n:nat
Z.abs_nat (Z.of_nat n) = n
 now rewrite <-Zabs_N_nat, <-nat_N_Z, Zabs2N.id, Nat2N.id.
Qed.

Z.abs_nat, basic equations

Lemma inj_0 : Z.abs_nat 0 = 0%nat.Z.abs_nat 0 = 0%nat
Proof.Z.abs_nat 0 = 0%nat
 reflexivity.
Qed.

Lemma inj_pos p : Z.abs_nat (Zpos p) = Pos.to_nat p.p:positive
Z.abs_nat (Z.pos p) = Pos.to_nat p
Proof.p:positive
Z.abs_nat (Z.pos p) = Pos.to_nat p
 reflexivity.
Qed.

Lemma inj_neg p : Z.abs_nat (Zneg p) = Pos.to_nat p.p:positive
Z.abs_nat (Z.neg p) = Pos.to_nat p
Proof.p:positive
Z.abs_nat (Z.neg p) = Pos.to_nat p
 reflexivity.
Qed.

Z.abs_nat and usual operations, with non-negative integers

Lemma inj_succ n : 0<=n -> Z.abs_nat (Z.succ n) = S (Z.abs_nat n).n:Z
0 <= n -> Z.abs_nat (Z.succ n) = S (Z.abs_nat n)
Proof.n:Z
0 <= n -> Z.abs_nat (Z.succ n) = S (Z.abs_nat n)
 intros.n:Z
H:0 <= n
Z.abs_nat (Z.succ n) = S (Z.abs_nat n) now rewrite <- !Zabs_N_nat, Zabs2N.inj_succ, N2Nat.inj_succ.
Qed.

Lemma inj_add n m : 0<=n -> 0<=m ->
 Z.abs_nat (n+m) = (Z.abs_nat n + Z.abs_nat m)%nat.n, m:Z
0 <= n ->
0 <= m ->
Z.abs_nat (n + m) = (Z.abs_nat n + Z.abs_nat m)%nat
Proof.n, m:Z
0 <= n ->
0 <= m ->
Z.abs_nat (n + m) = (Z.abs_nat n + Z.abs_nat m)%nat
 intros.n, m:Z
H:0 <= n
H0:0 <= m
Z.abs_nat (n + m) = (Z.abs_nat n + Z.abs_nat m)%nat now rewrite <- !Zabs_N_nat, Zabs2N.inj_add, N2Nat.inj_add.
Qed.

Lemma inj_mul n m : Z.abs_nat (n*m) = (Z.abs_nat n * Z.abs_nat m)%nat.n, m:Z
Z.abs_nat (n * m) = (Z.abs_nat n * Z.abs_nat m)%nat
Proof.n, m:Z
Z.abs_nat (n * m) = (Z.abs_nat n * Z.abs_nat m)%nat
 destruct n, m; simpl; trivial using Pos2Nat.inj_mul.
Qed.

Lemma inj_sub n m : 0<=m<=n ->
 Z.abs_nat (n-m) = (Z.abs_nat n - Z.abs_nat m)%nat.n, m:Z
0 <= m <= n ->
Z.abs_nat (n - m) = (Z.abs_nat n - Z.abs_nat m)%nat
Proof.n, m:Z
0 <= m <= n ->
Z.abs_nat (n - m) = (Z.abs_nat n - Z.abs_nat m)%nat
 intros.n, m:Z
H:0 <= m <= n
Z.abs_nat (n - m) = (Z.abs_nat n - Z.abs_nat m)%nat now rewrite <- !Zabs_N_nat, Zabs2N.inj_sub, N2Nat.inj_sub.
Qed.

Lemma inj_pred n : 0<n -> Z.abs_nat (Z.pred n) = Nat.pred (Z.abs_nat n).n:Z
0 < n -> Z.abs_nat (Z.pred n) = Nat.pred (Z.abs_nat n)
Proof.n:Z
0 < n -> Z.abs_nat (Z.pred n) = Nat.pred (Z.abs_nat n)
 intros.n:Z
H:0 < n
Z.abs_nat (Z.pred n) = Nat.pred (Z.abs_nat n) now rewrite <- !Zabs_N_nat, Zabs2N.inj_pred, N2Nat.inj_pred.
Qed.

Lemma inj_compare n m : 0<=n -> 0<=m ->
 (Z.abs_nat n ?= Z.abs_nat m)%nat = (n ?= m).n, m:Z
0 <= n ->
0 <= m -> (Z.abs_nat n ?= Z.abs_nat m)%nat = (n ?= m)
Proof.n, m:Z
0 <= n ->
0 <= m -> (Z.abs_nat n ?= Z.abs_nat m)%nat = (n ?= m)
 intros.n, m:Z
H:0 <= n
H0:0 <= m
(Z.abs_nat n ?= Z.abs_nat m)%nat = (n ?= m) now rewrite <- !Zabs_N_nat, <- N2Nat.inj_compare, Zabs2N.inj_compare.
Qed.

Lemma inj_le n m : 0<=n -> 0<=m -> (n<=m <-> (Z.abs_nat n <= Z.abs_nat m)%nat).n, m:Z
0 <= n ->
0 <= m -> n <= m <-> (Z.abs_nat n <= Z.abs_nat m)%nat
Proof.n, m:Z
0 <= n ->
0 <= m -> n <= m <-> (Z.abs_nat n <= Z.abs_nat m)%nat
 intros Hn Hm.n, m:Z
Hn:0 <= n
Hm:0 <= m
n <= m <-> (Z.abs_nat n <= Z.abs_nat m)%nat unfold Z.le.n, m:Z
Hn:0 <= n
Hm:0 <= m
(n ?= m) <> Gt <-> (Z.abs_nat n <= Z.abs_nat m)%nat now rewrite nat_compare_le, inj_compare.
Qed.

Lemma inj_lt n m : 0<=n -> 0<=m -> (n<m <-> (Z.abs_nat n < Z.abs_nat m)%nat).n, m:Z
0 <= n ->
0 <= m -> n < m <-> (Z.abs_nat n < Z.abs_nat m)%nat
Proof.n, m:Z
0 <= n ->
0 <= m -> n < m <-> (Z.abs_nat n < Z.abs_nat m)%nat
 intros Hn Hm.n, m:Z
Hn:0 <= n
Hm:0 <= m
n < m <-> (Z.abs_nat n < Z.abs_nat m)%nat unfold Z.lt.n, m:Z
Hn:0 <= n
Hm:0 <= m
(n ?= m) = Lt <-> (Z.abs_nat n < Z.abs_nat m)%nat now rewrite nat_compare_lt, inj_compare.
Qed.

Lemma inj_min n m : 0<=n -> 0<=m ->
 Z.abs_nat (Z.min n m) = Nat.min (Z.abs_nat n) (Z.abs_nat m).n, m:Z
0 <= n ->
0 <= m ->
Z.abs_nat (Z.min n m) =
Nat.min (Z.abs_nat n) (Z.abs_nat m)
Proof.n, m:Z
0 <= n ->
0 <= m ->
Z.abs_nat (Z.min n m) =
Nat.min (Z.abs_nat n) (Z.abs_nat m)
 intros.n, m:Z
H:0 <= n
H0:0 <= m
Z.abs_nat (Z.min n m) =
Nat.min (Z.abs_nat n) (Z.abs_nat m) now rewrite <- !Zabs_N_nat, Zabs2N.inj_min, N2Nat.inj_min.
Qed.

Lemma inj_max n m : 0<=n -> 0<=m ->
 Z.abs_nat (Z.max n m) = Nat.max (Z.abs_nat n) (Z.abs_nat m).n, m:Z
0 <= n ->
0 <= m ->
Z.abs_nat (Z.max n m) =
Nat.max (Z.abs_nat n) (Z.abs_nat m)
Proof.n, m:Z
0 <= n ->
0 <= m ->
Z.abs_nat (Z.max n m) =
Nat.max (Z.abs_nat n) (Z.abs_nat m)
 intros.n, m:Z
H:0 <= n
H0:0 <= m
Z.abs_nat (Z.max n m) =
Nat.max (Z.abs_nat n) (Z.abs_nat m) now rewrite <- !Zabs_N_nat, Zabs2N.inj_max, N2Nat.inj_max.
Qed.

Z.abs_nat and usual operations, statements with Z.abs

Lemma inj_succ_abs n : Z.abs_nat (Z.succ (Z.abs n)) = S (Z.abs_nat n).n:Z
Z.abs_nat (Z.succ (Z.abs n)) = S (Z.abs_nat n)
Proof.n:Z
Z.abs_nat (Z.succ (Z.abs n)) = S (Z.abs_nat n)
 now rewrite <- !Zabs_N_nat, Zabs2N.inj_succ_abs, N2Nat.inj_succ.
Qed.

Lemma inj_add_abs n m :
 Z.abs_nat (Z.abs n + Z.abs m) = (Z.abs_nat n + Z.abs_nat m)%nat.n, m:Z
Z.abs_nat (Z.abs n + Z.abs m) =
(Z.abs_nat n + Z.abs_nat m)%nat
Proof.n, m:Z
Z.abs_nat (Z.abs n + Z.abs m) =
(Z.abs_nat n + Z.abs_nat m)%nat
 now rewrite <- !Zabs_N_nat, Zabs2N.inj_add_abs, N2Nat.inj_add.
Qed.

Lemma inj_mul_abs n m :
 Z.abs_nat (Z.abs n * Z.abs m) = (Z.abs_nat n * Z.abs_nat m)%nat.n, m:Z
Z.abs_nat (Z.abs n * Z.abs m) =
(Z.abs_nat n * Z.abs_nat m)%nat
Proof.n, m:Z
Z.abs_nat (Z.abs n * Z.abs m) =
(Z.abs_nat n * Z.abs_nat m)%nat
 now rewrite <- !Zabs_N_nat, Zabs2N.inj_mul_abs, N2Nat.inj_mul.
Qed.

End Zabs2Nat.

Compatibility

Definition neq (x y:nat) := x <> y.

Lemma inj_neq n m : neq n m -> Zne (Z.of_nat n) (Z.of_nat m).n, m:nat
neq n m -> Zne (Z.of_nat n) (Z.of_nat m)
Proof.n, m:nat
neq n m -> Zne (Z.of_nat n) (Z.of_nat m) intros H H'.n, m:nat
H:neq n m
H':Z.of_nat n = Z.of_nat m
False now apply H, Nat2Z.inj. Qed.

Lemma Zpos_P_of_succ_nat n : Zpos (Pos.of_succ_nat n) = Z.succ (Z.of_nat n).n:nat
Z.pos (Pos.of_succ_nat n) = Z.succ (Z.of_nat n)
Proof (Nat2Z.inj_succ n).

For these one, used in omega, a Definition is necessary

Definition inj_eq := (f_equal Z.of_nat).
Definition inj_le n m := proj1 (Nat2Z.inj_le n m).
Definition inj_lt n m := proj1 (Nat2Z.inj_lt n m).
Definition inj_ge n m := proj1 (Nat2Z.inj_ge n m).
Definition inj_gt n m := proj1 (Nat2Z.inj_gt n m).

Register neq as plugins.omega.neq.
Register inj_eq as plugins.omega.inj_eq.
Register inj_neq as plugins.omega.inj_neq.
Register inj_le as plugins.omega.inj_le.
Register inj_lt as plugins.omega.inj_lt.
Register inj_ge as plugins.omega.inj_ge.
Register inj_gt as plugins.omega.inj_gt.

For the others, a Notation is fine

Notation inj_0 := Nat2Z.inj_0 (only parsing).
Notation inj_S := Nat2Z.inj_succ (only parsing).
Notation inj_compare := Nat2Z.inj_compare (only parsing).
Notation inj_eq_rev := Nat2Z.inj (only parsing).
Notation inj_eq_iff := (fun n m => iff_sym (Nat2Z.inj_iff n m)) (only parsing).
Notation inj_le_iff := Nat2Z.inj_le (only parsing).
Notation inj_lt_iff := Nat2Z.inj_lt (only parsing).
Notation inj_ge_iff := Nat2Z.inj_ge (only parsing).
Notation inj_gt_iff := Nat2Z.inj_gt (only parsing).
Notation inj_le_rev := (fun n m => proj2 (Nat2Z.inj_le n m)) (only parsing).
Notation inj_lt_rev := (fun n m => proj2 (Nat2Z.inj_lt n m)) (only parsing).
Notation inj_ge_rev := (fun n m => proj2 (Nat2Z.inj_ge n m)) (only parsing).
Notation inj_gt_rev := (fun n m => proj2 (Nat2Z.inj_gt n m)) (only parsing).
Notation inj_plus := Nat2Z.inj_add (only parsing).
Notation inj_mult := Nat2Z.inj_mul (only parsing).
Notation inj_minus1 := Nat2Z.inj_sub (only parsing).
Notation inj_minus := Nat2Z.inj_sub_max (only parsing).
Notation inj_min := Nat2Z.inj_min (only parsing).
Notation inj_max := Nat2Z.inj_max (only parsing).

Notation Z_of_nat_of_P := positive_nat_Z (only parsing).
Notation Zpos_eq_Z_of_nat_o_nat_of_P :=
  (fun p => eq_sym (positive_nat_Z p)) (only parsing).

Notation Z_of_nat_of_N := N_nat_Z (only parsing).
Notation Z_of_N_of_nat := nat_N_Z (only parsing).

Notation Z_of_N_eq := (f_equal Z.of_N) (only parsing).
Notation Z_of_N_eq_rev := N2Z.inj (only parsing).
Notation Z_of_N_eq_iff := (fun n m => iff_sym (N2Z.inj_iff n m)) (only parsing).
Notation Z_of_N_compare := N2Z.inj_compare (only parsing).
Notation Z_of_N_le_iff := N2Z.inj_le (only parsing).
Notation Z_of_N_lt_iff := N2Z.inj_lt (only parsing).
Notation Z_of_N_ge_iff := N2Z.inj_ge (only parsing).
Notation Z_of_N_gt_iff := N2Z.inj_gt (only parsing).
Notation Z_of_N_le := (fun n m => proj1 (N2Z.inj_le n m)) (only parsing).
Notation Z_of_N_lt := (fun n m => proj1 (N2Z.inj_lt n m)) (only parsing).
Notation Z_of_N_ge := (fun n m => proj1 (N2Z.inj_ge n m)) (only parsing).
Notation Z_of_N_gt := (fun n m => proj1 (N2Z.inj_gt n m)) (only parsing).
Notation Z_of_N_le_rev := (fun n m => proj2 (N2Z.inj_le n m)) (only parsing).
Notation Z_of_N_lt_rev := (fun n m => proj2 (N2Z.inj_lt n m)) (only parsing).
Notation Z_of_N_ge_rev := (fun n m => proj2 (N2Z.inj_ge n m)) (only parsing).
Notation Z_of_N_gt_rev := (fun n m => proj2 (N2Z.inj_gt n m)) (only parsing).
Notation Z_of_N_pos := N2Z.inj_pos (only parsing).
Notation Z_of_N_abs := N2Z.inj_abs_N (only parsing).
Notation Z_of_N_le_0 := N2Z.is_nonneg (only parsing).
Notation Z_of_N_plus := N2Z.inj_add (only parsing).
Notation Z_of_N_mult := N2Z.inj_mul (only parsing).
Notation Z_of_N_minus := N2Z.inj_sub_max (only parsing).
Notation Z_of_N_succ := N2Z.inj_succ (only parsing).
Notation Z_of_N_min := N2Z.inj_min (only parsing).
Notation Z_of_N_max := N2Z.inj_max (only parsing).
Notation Zabs_of_N := Zabs2N.id (only parsing).
Notation Zabs_N_succ_abs := Zabs2N.inj_succ_abs (only parsing).
Notation Zabs_N_succ := Zabs2N.inj_succ (only parsing).
Notation Zabs_N_plus_abs := Zabs2N.inj_add_abs (only parsing).
Notation Zabs_N_plus := Zabs2N.inj_add (only parsing).
Notation Zabs_N_mult_abs := Zabs2N.inj_mul_abs (only parsing).
Notation Zabs_N_mult := Zabs2N.inj_mul (only parsing).

Theorem inj_minus2 : forall n m:nat, (m > n)%nat -> Z.of_nat (n - m) = 0.forall n m : nat, (m > n)%nat -> Z.of_nat (n - m) = 0
Proof.forall n m : nat, (m > n)%nat -> Z.of_nat (n - m) = 0
 intros.n, m:nat
H:(m > n)%nat
Z.of_nat (n - m) = 0 rewrite not_le_minus_0; auto with arith.
Qed.

Register inj_minus2 as plugins.omega.inj_minus2.