Modularisation of Znat, a few name changed elsewhere

 For instance inj_plus is now Nat2Z.inj_add

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14108 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 808 insertions, 308 deletions

diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v
index ccf1e9dc6..133d4c23b 100644
--- a/theories/NArith/Nnat.v
+++ b/theories/NArith/Nnat.v
@@ -15,20 +15,25 @@ Module N2Nat.
 
 (** [N.to_nat] is a bijection between [N] and [nat],
     with [Pos.of_nat] as reciprocal.
-    See [Nat2N.bij] below for the dual equation. *)
+    See [Nat2N.id] below for the dual equation. *)
 
-Lemma bij a : N.of_nat (N.to_nat a) = a.
+Lemma id a : N.of_nat (N.to_nat a) = a.
 Proof.
  destruct a as [| p]; simpl; trivial.
  destruct (Pos2Nat.is_succ p) as (n,H). rewrite H. simpl. f_equal.
- apply Pos2Nat.inj. rewrite H. apply SuccNat2Pos.bij.
+ apply Pos2Nat.inj. rewrite H. apply SuccNat2Pos.id_succ.
 Qed.
 
 (** [N.to_nat] is hence injective *)
 
 Lemma inj a a' : N.to_nat a = N.to_nat a' -> a = a'.
 Proof.
- intro H. rewrite <- (bij a), <- (bij a'). now f_equal.
+ intro H. rewrite <- (id a), <- (id a'). now f_equal.
+Qed.
+
+Lemma inj_iff a a' : N.to_nat a = N.to_nat a' <-> a = a'.
+Proof.
+ split. apply inj. intros; now subst.
 Qed.
 
 (** Interaction of this translation and usual operations. *)
@@ -85,7 +90,7 @@ Proof.
 Qed.
 
 Lemma inj_compare a a' :
- N.compare a a' = nat_compare (N.to_nat a) (N.to_nat a').
+ (a ?= a')%N = nat_compare (N.to_nat a) (N.to_nat a').
 Proof.
  destruct a, a'; simpl; trivial.
  now destruct (Pos2Nat.is_succ p) as (n,->).
@@ -118,7 +123,7 @@ End N2Nat.
 Hint Rewrite N2Nat.inj_double N2Nat.inj_succ_double
  N2Nat.inj_succ N2Nat.inj_add N2Nat.inj_mul N2Nat.inj_sub
  N2Nat.inj_pred N2Nat.inj_div2 N2Nat.inj_max N2Nat.inj_min
- N2Nat.bij
+ N2Nat.id
  : Nnat.
 
 
@@ -126,23 +131,28 @@ Hint Rewrite N2Nat.inj_double N2Nat.inj_succ_double
 
 Module Nat2N.
 
-(** [N.of_nat] is a bijection between [nat] and [N],
+(** [N.of_nat] is an bijection between [nat] and [N],
     with [Pos.to_nat] as reciprocal.
-    See [N2Nat.bij] above for the dual equation. *)
+    See [N2Nat.id] above for the dual equation. *)
 
-Lemma bij n : N.to_nat (N.of_nat n) = n.
+Lemma id n : N.to_nat (N.of_nat n) = n.
 Proof.
- induction n; simpl; trivial. apply SuccNat2Pos.bij.
+ induction n; simpl; trivial. apply SuccNat2Pos.id_succ.
 Qed.
 
-Hint Rewrite bij : Nnat.
+Hint Rewrite id : Nnat.
 Ltac nat2N := apply N2Nat.inj; now autorewrite with Nnat.
 
 (** [N.of_nat] is hence injective *)
 
 Lemma inj n n' : N.of_nat n = N.of_nat n' -> n = n'.
 Proof.
- intros H. rewrite <- (bij n), <- (bij n'). now f_equal.
+ intros H. rewrite <- (id n), <- (id n'). now f_equal.
+Qed.
+
+Lemma inj_iff n n' : N.of_nat n = N.of_nat n' <-> n = n'.
+Proof.
+ split. apply inj. intros; now subst.
 Qed.
 
 (** Interaction of this translation and usual operations. *)
@@ -172,8 +182,8 @@ Lemma inj_div2 n : N.of_nat (div2 n) = N.div2 (N.of_nat n).
 Proof. nat2N. Qed.
 
 Lemma inj_compare n n' :
-  nat_compare n n' = N.compare (N.of_nat n) (N.of_nat n').
-Proof. now rewrite N2Nat.inj_compare, !bij. Qed.
+  nat_compare n n' = (N.of_nat n ?= N.of_nat n')%N.
+Proof. now rewrite N2Nat.inj_compare, !id. Qed.
 
 Lemma inj_min n n' :
   N.of_nat (min n n') = N.min (N.of_nat n) (N.of_nat n').
@@ -185,16 +195,16 @@ Proof. nat2N. Qed.
 
 Lemma inj_iter n {A} (f:A->A) (x:A) :
   nat_iter n f x = N.iter (N.of_nat n) f x.
-Proof. now rewrite N2Nat.inj_iter, !bij. Qed.
+Proof. now rewrite N2Nat.inj_iter, !id. Qed.
 
 End Nat2N.
 
-Hint Rewrite Nat2N.bij : Nnat.
+Hint Rewrite Nat2N.id : Nnat.
 
 (** Compatibility notations *)
 
 Notation nat_of_N_inj := N2Nat.inj (only parsing).
-Notation N_of_nat_of_N := N2Nat.bij (only parsing).
+Notation N_of_nat_of_N := N2Nat.id (only parsing).
 Notation nat_of_Ndouble := N2Nat.inj_double (only parsing).
 Notation nat_of_Ndouble_plus_one := N2Nat.inj_succ_double (only parsing).
 Notation nat_of_Nsucc := N2Nat.inj_succ (only parsing).
@@ -207,7 +217,7 @@ Notation nat_of_Ncompare := N2Nat.inj_compare (only parsing).
 Notation nat_of_Nmax := N2Nat.inj_max (only parsing).
 Notation nat_of_Nmin := N2Nat.inj_min (only parsing).
 
-Notation nat_of_N_of_nat := Nat2N.bij (only parsing).
+Notation nat_of_N_of_nat := Nat2N.id (only parsing).
 Notation N_of_nat_inj := Nat2N.inj (only parsing).
 Notation N_of_double := Nat2N.inj_double (only parsing).
 Notation N_of_double_plus_one := Nat2N.inj_succ_double (only parsing).
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 19c10f87d..a6988f0af 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -1566,20 +1566,19 @@ Qed.
 
 (** ** Results about [of_nat] and [of_succ_nat] *)
 
+Lemma of_nat_succ (n:nat) : of_succ_nat n = of_nat (S n).
+Proof.
+ induction n. trivial. simpl. f_equal. now rewrite IHn.
+Qed.
+
 Lemma pred_of_succ_nat (n:nat) : pred (of_succ_nat n) = of_nat n.
 Proof.
- induction n. trivial.
- simpl. rewrite pred_succ. rewrite <- IHn.
- destruct n. trivial.
- simpl. now rewrite pred_succ.
+ destruct n. trivial. simpl pred. rewrite pred_succ. apply of_nat_succ.
 Qed.
 
 Lemma succ_of_nat (n:nat) : n<>O -> succ (of_nat n) = of_succ_nat n.
 Proof.
- intro H.
- rewrite <- pred_of_succ_nat.
- destruct n. now destruct H.
- simpl. now rewrite pred_succ.
+ rewrite of_nat_succ. destruct n; trivial. now destruct 1.
 Qed.
 
 (** ** Correctness proofs for the square root function *)
diff --git a/theories/PArith/Pnat.v b/theories/PArith/Pnat.v
index a0ca9f5b6..f9df70bd3 100644
--- a/theories/PArith/Pnat.v
+++ b/theories/PArith/Pnat.v
@@ -76,9 +76,9 @@ Qed.
 
 (** [Pos.to_nat] is a bijection between [positive] and
     non-zero [nat], with [Pos.of_nat] as reciprocal.
-    See [Nat2Pos.bij] below for the dual equation. *)
+    See [Nat2Pos.id] below for the dual equation. *)
 
-Theorem bij p : of_nat (to_nat p) = p.
+Theorem id p : of_nat (to_nat p) = p.
 Proof.
  induction p using peano_ind. trivial.
  rewrite inj_succ. rewrite <- IHp at 2.
@@ -89,7 +89,7 @@ Qed.
 
 Lemma inj p q : to_nat p = to_nat q -> p = q.
 Proof.
- intros H. now rewrite <- (bij p), <- (bij q), H.
+ intros H. now rewrite <- (id p), <- (id q), H.
 Qed.
 
 Lemma inj_iff p q : to_nat p = to_nat q <-> p = q.
@@ -143,7 +143,52 @@ Proof.
  now apply lt_le_weak, inj_lt.
 Qed.
 
-(** [Pos.to_nat] is a morphism for [Pos.iter] and [nat_iter] *)
+Theorem inj_sub_max p q :
+ to_nat (p - q) = Peano.max 1 (to_nat p - to_nat q).
+Proof.
+ destruct (ltb_spec q p).
+ rewrite <- inj_sub by trivial.
+ now destruct (is_succ (p - q)) as (m,->).
+ rewrite sub_le by trivial.
+ replace (to_nat p - to_nat q) with 0; trivial.
+ apply le_n_0_eq.
+ rewrite <- (minus_diag (to_nat p)).
+ now apply minus_le_compat_l, inj_le.
+Qed.
+
+Theorem inj_pred p : (1 < p)%positive ->
+ to_nat (pred p) = Peano.pred (to_nat p).
+Proof.
+ intros H. now rewrite <- Pos.sub_1_r, inj_sub, pred_of_minus.
+Qed.
+
+Theorem inj_pred_max p :
+ to_nat (pred p) = Peano.max 1 (Peano.pred (to_nat p)).
+Proof.
+ rewrite <- Pos.sub_1_r, pred_of_minus. apply inj_sub_max.
+Qed.
+
+(** [Pos.to_nat] and other operations *)
+
+Lemma inj_min p q :
+ to_nat (min p q) = Peano.min (to_nat p) (to_nat q).
+Proof.
+ unfold min. rewrite inj_compare.
+ case nat_compare_spec; intros H; symmetry.
+ apply Peano.min_l. now rewrite H.
+ now apply Peano.min_l, lt_le_weak.
+ now apply Peano.min_r, lt_le_weak.
+Qed.
+
+Lemma inj_max p q :
+ to_nat (max p q) = Peano.max (to_nat p) (to_nat q).
+Proof.
+ unfold max. rewrite inj_compare.
+ case nat_compare_spec; intros H; symmetry.
+ apply Peano.max_r. now rewrite H.
+ now apply Peano.max_r, lt_le_weak.
+ now apply Peano.max_l, lt_le_weak.
+Qed.
 
 Theorem inj_iter :
   forall p {A} (f:A->A) (x:A),
@@ -159,20 +204,25 @@ Module Nat2Pos.
 
 (** [Pos.of_nat] is a bijection between non-zero [nat] and
     [positive], with [Pos.to_nat] as reciprocal.
-    See [Pos2Nat.bij] above for the dual equation. *)
+    See [Pos2Nat.id] above for the dual equation. *)
 
-Theorem bij (n:nat) : n<>0 -> Pos.to_nat (Pos.of_nat n) = n.
+Theorem id (n:nat) : n<>0 -> Pos.to_nat (Pos.of_nat n) = n.
 Proof.
  induction n as [|n H]; trivial. now destruct 1.
  intros _. simpl. destruct n. trivial.
  rewrite Pos2Nat.inj_succ. f_equal. now apply H.
 Qed.
 
+Theorem id_max (n:nat) : Pos.to_nat (Pos.of_nat n) = max 1 n.
+Proof.
+ destruct n. trivial. now rewrite id.
+Qed.
+
 (** [Pos.of_nat] is hence injective for non-zero numbers *)
 
 Lemma inj (n m : nat) : n<>0 -> m<>0 -> Pos.of_nat n = Pos.of_nat m -> n = m.
 Proof.
- intros Hn Hm H. now rewrite <- (bij n), <- (bij m), H.
+ intros Hn Hm H. now rewrite <- (id n), <- (id m), H.
 Qed.
 
 Lemma inj_iff (n m : nat) : n<>0 -> m<>0 ->
@@ -186,14 +236,19 @@ Qed.
 
 Lemma inj_succ (n:nat) : n<>0 -> Pos.of_nat (S n) = Pos.succ (Pos.of_nat n).
 Proof.
-intro H. apply Pos2Nat.inj. now rewrite Pos2Nat.inj_succ, !bij.
+intro H. apply Pos2Nat.inj. now rewrite Pos2Nat.inj_succ, !id.
+Qed.
+
+Lemma inj_pred (n:nat) : Pos.of_nat (pred n) = Pos.pred (Pos.of_nat n).
+Proof.
+ destruct n as [|[|n]]; trivial. simpl. now rewrite Pos.pred_succ.
 Qed.
 
 Lemma inj_add (n m : nat) : n<>0 -> m<>0 ->
  Pos.of_nat (n+m) = (Pos.of_nat n + Pos.of_nat m)%positive.
 Proof.
 intros Hn Hm. apply Pos2Nat.inj.
-rewrite Pos2Nat.inj_add, !bij; trivial.
+rewrite Pos2Nat.inj_add, !id; trivial.
 intros H. destruct n. now destruct Hn. now simpl in H.
 Qed.
 
@@ -201,14 +256,44 @@ Lemma inj_mul (n m : nat) : n<>0 -> m<>0 ->
  Pos.of_nat (n*m) = (Pos.of_nat n * Pos.of_nat m)%positive.
 Proof.
 intros Hn Hm. apply Pos2Nat.inj.
-rewrite Pos2Nat.inj_mul, !bij; trivial.
+rewrite Pos2Nat.inj_mul, !id; trivial.
 intros H. apply mult_is_O in H. destruct H. now elim Hn. now elim Hm.
 Qed.
 
 Lemma inj_compare (n m : nat) : n<>0 -> m<>0 ->
  nat_compare n m = (Pos.of_nat n ?= Pos.of_nat m).
 Proof.
-intros Hn Hm. rewrite Pos2Nat.inj_compare, !bij; trivial.
+intros Hn Hm. rewrite Pos2Nat.inj_compare, !id; trivial.
+Qed.
+
+Lemma inj_sub (n m : nat) : m<>0 ->
+ Pos.of_nat (n-m) = (Pos.of_nat n - Pos.of_nat m)%positive.
+Proof.
+ intros Hm.
+ apply Pos2Nat.inj.
+ rewrite Pos2Nat.inj_sub_max.
+ rewrite (id m) by trivial. rewrite !id_max.
+ destruct n, m; trivial.
+Qed.
+
+Lemma inj_min (n m : nat) :
+ Pos.of_nat (min n m) = Pos.min (Pos.of_nat n) (Pos.of_nat m).
+Proof.
+ destruct n as [|n]. simpl. symmetry. apply Pos.min_l, Pos.le_1_l.
+ destruct m as [|m]. simpl. symmetry. apply Pos.min_r, Pos.le_1_l.
+ unfold Pos.min. rewrite <- inj_compare by easy.
+ case nat_compare_spec; intros H; f_equal; apply min_l || apply min_r.
+ rewrite H; auto. now apply lt_le_weak. now apply lt_le_weak.
+Qed.
+
+Lemma inj_max (n m : nat) :
+ Pos.of_nat (max n m) = Pos.max (Pos.of_nat n) (Pos.of_nat m).
+Proof.
+ destruct n as [|n]. simpl. symmetry. apply Pos.max_r, Pos.le_1_l.
+ destruct m as [|m]. simpl. symmetry. apply Pos.max_l, Pos.le_1_l.
+ unfold Pos.max. rewrite <- inj_compare by easy.
+ case nat_compare_spec; intros H; f_equal; apply max_l || apply max_r.
+ rewrite H; auto. now apply lt_le_weak. now apply lt_le_weak.
 Qed.
 
 End Nat2Pos.
@@ -222,18 +307,17 @@ Module Pos2SuccNat.
 (** Composition of [Pos.to_nat] and [Pos.of_succ_nat] is successor
     on [positive] *)
 
-Theorem bij p : Pos.of_succ_nat (Pos.to_nat p) = Pos.succ p.
+Theorem id_succ p : Pos.of_succ_nat (Pos.to_nat p) = Pos.succ p.
 Proof.
-induction p using Pos.peano_ind. trivial.
-rewrite Pos2Nat.inj_succ. simpl. now f_equal.
+rewrite Pos.of_nat_succ, <- Pos2Nat.inj_succ. apply Pos2Nat.id.
 Qed.
 
 (** Composition of [Pos.to_nat], [Pos.of_succ_nat] and [Pos.pred]
     is identity on [positive] *)
 
-Theorem bij' p : Pos.pred (Pos.of_succ_nat (Pos.to_nat p)) = p.
+Theorem pred_id p : Pos.pred (Pos.of_succ_nat (Pos.to_nat p)) = p.
 Proof.
-now rewrite bij, Pos.pred_succ.
+now rewrite id_succ, Pos.pred_succ.
 Qed.
 
 End Pos2SuccNat.
@@ -242,16 +326,21 @@ Module SuccNat2Pos.
 
 (** Composition of [Pos.of_succ_nat] and [Pos.to_nat] is successor on [nat] *)
 
-Theorem bij (n:nat) : Pos.to_nat (Pos.of_succ_nat n) = S n.
+Theorem id_succ (n:nat) : Pos.to_nat (Pos.of_succ_nat n) = S n.
+Proof.
+rewrite Pos.of_nat_succ. now apply Nat2Pos.id.
+Qed.
+
+Theorem pred_id (n:nat) : pred (Pos.to_nat (Pos.of_succ_nat n)) = n.
 Proof.
-induction n as [|n H]; trivial; simpl; now rewrite Pos2Nat.inj_succ, H.
+now rewrite id_succ.
 Qed.
 
 (** [Pos.of_succ_nat] is hence injective *)
 
 Lemma inj (n m : nat) : Pos.of_succ_nat n = Pos.of_succ_nat m -> n = m.
 Proof.
- intro H. apply (f_equal Pos.to_nat) in H. rewrite !bij in H.
+ intro H. apply (f_equal Pos.to_nat) in H. rewrite !id_succ in H.
  now injection H.
 Qed.
 
@@ -260,18 +349,25 @@ Proof.
  split. apply inj. intros; now subst.
 Qed.
 
+(** Another formulation *)
+
+Theorem inv n p : Pos.to_nat p = S n -> Pos.of_succ_nat n = p.
+Proof.
+ intros H. apply Pos2Nat.inj. now rewrite id_succ.
+Qed.
+
 (** Successor and comparison are morphisms with respect to
     [Pos.of_succ_nat] *)
 
 Lemma inj_succ n : Pos.of_succ_nat (S n) = Pos.succ (Pos.of_succ_nat n).
 Proof.
-apply Pos2Nat.inj. now rewrite Pos2Nat.inj_succ, !bij.
+apply Pos2Nat.inj. now rewrite Pos2Nat.inj_succ, !id_succ.
 Qed.
 
 Lemma inj_compare n m :
  nat_compare n m = (Pos.of_succ_nat n ?= Pos.of_succ_nat m).
 Proof.
-rewrite Pos2Nat.inj_compare, !bij; trivial.
+rewrite Pos2Nat.inj_compare, !id_succ; trivial.
 Qed.
 
 (** Other operations, for instance [Pos.add] and [plus] aren't
@@ -300,8 +396,8 @@ Notation Pge_ge := Pos2Nat.inj_ge (only parsing).
 Notation Pminus_minus := Pos2Nat.inj_sub (only parsing).
 Notation iter_nat_of_P := @Pos2Nat.inj_iter (only parsing).
 
-Notation nat_of_P_of_succ_nat := SuccNat2Pos.bij (only parsing).
-Notation P_of_succ_nat_of_P := Pos2SuccNat.bij (only parsing).
+Notation nat_of_P_of_succ_nat := SuccNat2Pos.id_succ (only parsing).
+Notation P_of_succ_nat_of_P := Pos2SuccNat.id_succ (only parsing).
 
 Notation nat_of_P_succ_morphism := Pos2Nat.inj_succ (only parsing).
 Notation nat_of_P_plus_morphism := Pos2Nat.inj_add (only parsing).
@@ -309,9 +405,9 @@ Notation nat_of_P_mult_morphism := Pos2Nat.inj_mul (only parsing).
 Notation nat_of_P_compare_morphism := Pos2Nat.inj_compare (only parsing).
 Notation lt_O_nat_of_P := Pos2Nat.is_pos (only parsing).
 Notation ZL4 := Pos2Nat.is_succ (only parsing).
-Notation nat_of_P_o_P_of_succ_nat_eq_succ := SuccNat2Pos.bij (only parsing).
-Notation P_of_succ_nat_o_nat_of_P_eq_succ := Pos2SuccNat.bij (only parsing).
-Notation pred_o_P_of_succ_nat_o_nat_of_P_eq_id := Pos2SuccNat.bij' (only parsing).
+Notation nat_of_P_o_P_of_succ_nat_eq_succ := SuccNat2Pos.id_succ (only parsing).
+Notation P_of_succ_nat_o_nat_of_P_eq_succ := Pos2SuccNat.id_succ (only parsing).
+Notation pred_o_P_of_succ_nat_o_nat_of_P_eq_id := Pos2SuccNat.pred_id (only parsing).
 
 Lemma nat_of_P_minus_morphism p q :
  Pcompare p q Eq = Gt -> Pos.to_nat (p - q) = Pos.to_nat p - Pos.to_nat q.
diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v
index 77cae88fe..4941dedb2 100644
--- a/theories/ZArith/Zabs.v
+++ b/theories/ZArith/Zabs.v
@@ -16,7 +16,7 @@ Require Import Zorder.
 Require Import Znat.
 Require Import ZArith_dec.
 
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 (**********************************************************************)
 (** * Properties of absolute value *)
@@ -115,71 +115,6 @@ Proof.
   destruct a; simpl; auto.
 Qed.
 
-(** * Results about absolute value in nat. *)
-
-Theorem inj_Zabs_nat : forall z:Z, Z_of_nat (Zabs_nat z) = Zabs z.
-Proof.
-  destruct z; simpl; auto; symmetry; apply Zpos_eq_Z_of_nat_o_nat_of_P.
-Qed.
-
-Theorem Zabs_nat_Z_of_nat: forall n, Zabs_nat (Z_of_nat n) = n.
-Proof.
-  destruct n; simpl; auto.
-  apply nat_of_P_of_succ_nat.
-Qed.
-
-Lemma Zabs_nat_mult: forall n m:Z, Zabs_nat (n*m) = (Zabs_nat n * Zabs_nat m)%nat.
-Proof.
-  intros; apply inj_eq_rev.
-  rewrite inj_mult; repeat rewrite inj_Zabs_nat; apply Zabs_Zmult.
-Qed.
-
-Lemma Zabs_nat_Zsucc:
- forall p, 0 <= p ->  Zabs_nat (Zsucc p) = S (Zabs_nat p).
-Proof.
-  intros; apply inj_eq_rev.
-  rewrite inj_S; repeat rewrite inj_Zabs_nat, Zabs_eq; auto with zarith.
-Qed.
-
-Lemma Zabs_nat_Zplus:
- forall x y, 0<=x -> 0<=y -> Zabs_nat (x+y) = (Zabs_nat x + Zabs_nat y)%nat.
-Proof.
-  intros; apply inj_eq_rev.
-  rewrite inj_plus; repeat rewrite inj_Zabs_nat, Zabs_eq; auto with zarith.
-  apply Zplus_le_0_compat; auto.
-Qed.
-
-Lemma Zabs_nat_compare :
- forall x y, 0<=x -> 0<=y -> nat_compare (Zabs_nat x) (Zabs_nat y) = (x?=y).
-Proof.
- intros. rewrite <- inj_compare, 2 inj_Zabs_nat, 2 Zabs_eq; trivial.
-Qed.
-
-Lemma Zabs_nat_le :
-  forall n m:Z, 0 <= n <= m -> (Zabs_nat n <= Zabs_nat m)%nat.
-Proof.
- intros n m (H,H'). apply nat_compare_le. rewrite Zabs_nat_compare; trivial.
- apply Zle_trans with n; auto.
-Qed.
-
-Lemma Zabs_nat_lt :
-  forall n m:Z, 0 <= n < m -> (Zabs_nat n < Zabs_nat m)%nat.
-Proof.
-  intros n m (H,H'). apply nat_compare_lt. rewrite Zabs_nat_compare; trivial.
-  apply Zlt_le_weak; apply Zle_lt_trans with n; auto.
-Qed.
-
-Lemma Zabs_nat_Zminus:
- forall x y, 0 <= x <= y ->  Zabs_nat (y - x) = (Zabs_nat y - Zabs_nat x)%nat.
-Proof.
-  intros x y (H,H').
-  assert (0 <= y) by (apply Zle_trans with x; auto).
-  assert (0 <= y-x) by (apply Zle_minus_le_0; auto).
-  apply inj_eq_rev.
-  rewrite inj_minus1. rewrite !inj_Zabs_nat, !Zabs_eq; auto.
-  apply Zabs_nat_le. now split.
-Qed.
-
 (** * Some results about the sign function. *)
 
 Lemma Zsgn_Zmult : forall a b, Zsgn (a*b) = Zsgn a * Zsgn b.
@@ -217,3 +152,26 @@ Proof.
  destruct x; now intuition.
 Qed.
 
+(** Compatibility *)
+
+Notation inj_Zabs_nat := Zabs2Nat.id_abs (only parsing).
+Notation Zabs_nat_Z_of_nat := Zabs2Nat.id (only parsing).
+Notation Zabs_nat_mult := Zabs2Nat.inj_mul (only parsing).
+Notation Zabs_nat_Zsucc := Zabs2Nat.inj_succ (only parsing).
+Notation Zabs_nat_Zplus := Zabs2Nat.inj_add (only parsing).
+Notation Zabs_nat_Zminus := (fun n m => Zabs2Nat.inj_sub m n) (only parsing).
+Notation Zabs_nat_compare := Zabs2Nat.inj_compare (only parsing).
+
+Lemma Zabs_nat_le :
+  forall n m:Z, 0 <= n <= m -> (Zabs_nat n <= Zabs_nat m)%nat.
+Proof.
+ intros n m (H,H'). apply nat_compare_le. rewrite Zabs_nat_compare; trivial.
+ apply Zle_trans with n; auto.
+Qed.
+
+Lemma Zabs_nat_lt :
+  forall n m:Z, 0 <= n < m -> (Zabs_nat n < Zabs_nat m)%nat.
+Proof.
+  intros n m (H,H'). apply nat_compare_lt. rewrite Zabs_nat_compare; trivial.
+  apply Zlt_le_weak; apply Zle_lt_trans with n; auto.
+Qed.
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index 353ab602e..2fdfad5dd 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -10,382 +10,819 @@
 (** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
 
 Require Export Arith_base.
-Require Import BinPos BinInt BinNat Zcompare Zorder.
-Require Import Decidable Peano_dec Min Max Compare_dec.
+Require Import BinPos BinInt BinNat Pnat Nnat.
 
 Local Open Scope Z_scope.
 
-Definition neq (x y:nat) := x <> y.
+(** * Chains of conversions *)
 
-(************************************************)
-(** Properties of the injection from nat into Z *)
+(** When combining successive conversions, we have the following
+    commutative diagram:
+<<
+      ---> Nat ----
+     |      ^      |
+     |      |      v
+    Pos ---------> Z
+     |      |      ^
+     |      v      |
+      ----> N -----
+>>
+*)
 
-Lemma Zpos_P_of_succ_nat : forall n:nat,
- Zpos (P_of_succ_nat n) = Zsucc (Z_of_nat n).
+Lemma nat_N_Z n : Z.of_N (N.of_nat n) = Z.of_nat n.
 Proof.
-  intros [|n]. trivial. apply Zpos_succ_morphism.
+ now destruct n.
 Qed.
 
-(** Injection and successor *)
-
-Theorem inj_0 : Z_of_nat 0 = 0.
+Lemma N_nat_Z n : Z.of_nat (N.to_nat n) = Z.of_N n.
 Proof.
-  reflexivity.
+ destruct n; trivial. simpl.
+ destruct (Pos2Nat.is_succ p) as (m,H).
+ rewrite H. simpl. f_equal. now apply SuccNat2Pos.inv.
 Qed.
 
-Theorem inj_S : forall n:nat, Z_of_nat (S n) = Zsucc (Z_of_nat n).
+Lemma positive_nat_Z p : Z.of_nat (Pos.to_nat p) = Zpos p.
 Proof.
-  exact Zpos_P_of_succ_nat.
+ destruct (Pos2Nat.is_succ p) as (n,H).
+ rewrite H. simpl. f_equal. now apply SuccNat2Pos.inv.
 Qed.
 
-(** Injection and comparison *)
+Lemma positive_N_Z p : Z.of_N (Npos p) = Zpos p.
+Proof.
+ reflexivity.
+Qed.
 
-Theorem inj_compare : forall n m:nat,
- (Z_of_nat n ?= Z_of_nat m) = nat_compare n m.
+Lemma positive_N_nat p : N.to_nat (Npos p) = Pos.to_nat p.
 Proof.
- induction n; destruct m; trivial.
- rewrite 2 inj_S, Zcompare_succ_compat. now simpl.
+ reflexivity.
 Qed.
 
-(** Injection and equality. *)
+Lemma positive_nat_N p : N.of_nat (Pos.to_nat p) = Npos p.
+Proof.
+ destruct (Pos2Nat.is_succ p) as (n,H).
+ rewrite H. simpl. f_equal. now apply SuccNat2Pos.inv.
+Qed.
 
-Theorem inj_eq : forall n m:nat, n = m -> Z_of_nat n = Z_of_nat m.
+Lemma Z_N_nat n : N.to_nat (Z.to_N n) = Z.to_nat n.
 Proof.
-  intros; subst; trivial.
+ now destruct n.
 Qed.
 
-Theorem inj_eq_rev : forall n m:nat, Z_of_nat n = Z_of_nat m -> n = m.
+Lemma Z_nat_N n : N.of_nat (Z.to_nat n) = Z.to_N n.
 Proof.
-  intros n m H. apply nat_compare_eq.
-  now rewrite <- inj_compare, H, Zcompare_refl.
+ destruct n; simpl; trivial. apply positive_nat_N.
 Qed.
 
-Theorem inj_neq : forall n m:nat, neq n m -> Zne (Z_of_nat n) (Z_of_nat m).
+Lemma Zabs_N_nat n : N.to_nat (Z.abs_N n) = Z.abs_nat n.
 Proof.
-  unfold neq, Zne. intros n m H. contradict H. now apply inj_eq_rev.
+ now destruct n.
 Qed.
 
-Theorem inj_eq_iff : forall n m:nat, n=m <-> Z_of_nat n = Z_of_nat m.
+Lemma Zabs_nat_N n : N.of_nat (Z.abs_nat n) = Z.abs_N n.
 Proof.
- split; [apply inj_eq | apply inj_eq_rev].
+ destruct n; simpl; trivial; apply positive_nat_N.
 Qed.
 
-(** Injection and order *)
 
-(** Both ways ... *)
+(** * Conversions between [Z] and [N] *)
+
+Module N2Z.
 
-Theorem inj_le_iff : forall n m:nat, (n<=m)%nat <-> Z_of_nat n <= Z_of_nat m.
+(** [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.
 Proof.
- intros. unfold Zle. rewrite inj_compare. apply nat_compare_le.
+ now destruct n.
 Qed.
 
-Theorem inj_lt_iff : forall n m:nat, (n<m)%nat <-> Z_of_nat n < Z_of_nat m.
+(** [Z.of_N] is hence injective *)
+
+Lemma inj n m : Z.of_N n = Z.of_N m -> n = m.
 Proof.
- intros. unfold Zlt. rewrite inj_compare. apply nat_compare_lt.
+ destruct n, m; simpl; congruence.
 Qed.
 
-Theorem inj_ge_iff : forall n m:nat, (n>=m)%nat <-> Z_of_nat n >= Z_of_nat m.
+Lemma inj_iff n m : Z.of_N n = Z.of_N m <-> n = m.
 Proof.
- intros. unfold Zge. rewrite inj_compare. apply nat_compare_ge.
+ split. apply inj. intros; now f_equal.
 Qed.
 
-Theorem inj_gt_iff : forall n m:nat, (n>m)%nat <-> Z_of_nat n > Z_of_nat m.
+(** [Z.of_N] produce non-negative integers *)
+
+Lemma is_nonneg n : 0 <= Z.of_N n.
 Proof.
- intros. unfold Zgt. rewrite inj_compare. apply nat_compare_gt.
+ now destruct n.
 Qed.
 
-(** One way ... *)
+(** [Z.of_N], basic equations *)
 
-Theorem inj_le : forall n m:nat, (n <= m)%nat -> Z_of_nat n <= Z_of_nat m.
-Proof. apply inj_le_iff. Qed.
+Lemma inj_0 : Z.of_N 0 = 0.
+Proof.
+ reflexivity.
+Qed.
 
-Theorem inj_lt : forall n m:nat, (n < m)%nat -> Z_of_nat n < Z_of_nat m.
-Proof. apply inj_lt_iff. Qed.
+Lemma inj_pos p : Z.of_N (Npos p) = Zpos p.
+Proof.
+ reflexivity.
+Qed.
 
-Theorem inj_ge : forall n m:nat, (n >= m)%nat -> Z_of_nat n >= Z_of_nat m.
-Proof. apply inj_ge_iff. Qed.
+(** [Z.of_N] and usual operations. *)
 
-Theorem inj_gt : forall n m:nat, (n > m)%nat -> Z_of_nat n > Z_of_nat m.
-Proof. apply inj_gt_iff. Qed.
+Lemma inj_compare n m : (Z.of_N n ?= Z.of_N m) = (n ?= m)%N.
+Proof.
+ now destruct n, m.
+Qed.
 
-(** The other way ... *)
+Lemma inj_le n m : (n<=m)%N <-> Z.of_N n <= Z.of_N m.
+Proof.
+ unfold Z.le. now rewrite inj_compare.
+Qed.
 
-Theorem inj_le_rev : forall n m:nat, Z_of_nat n <= Z_of_nat m -> (n <= m)%nat.
-Proof. apply inj_le_iff. Qed.
+Lemma inj_lt n m : (n<m)%N <-> Z.of_N n < Z.of_N m.
+Proof.
+ unfold Z.lt. now rewrite inj_compare.
+Qed.
 
-Theorem inj_lt_rev : forall n m:nat, Z_of_nat n < Z_of_nat m -> (n < m)%nat.
-Proof. apply inj_lt_iff. Qed.
+Lemma inj_ge n m : (n>=m)%N <-> Z.of_N n >= Z.of_N m.
+Proof.
+ unfold Z.ge. now rewrite inj_compare.
+Qed.
 
-Theorem inj_ge_rev : forall n m:nat, Z_of_nat n >= Z_of_nat m -> (n >= m)%nat.
-Proof. apply inj_ge_iff. Qed.
+Lemma inj_gt n m : (n>m)%N <-> Z.of_N n > Z.of_N m.
+Proof.
+ unfold Z.gt. now rewrite inj_compare.
+Qed.
+
+Lemma inj_abs_N z : Z.of_N (Z.abs_N z) = Z.abs z.
+Proof.
+ now destruct z.
+Qed.
 
-Theorem inj_gt_rev : forall n m:nat, Z_of_nat n > Z_of_nat m -> (n > m)%nat.
-Proof. apply inj_gt_iff. Qed.
+Lemma inj_add n m : Z.of_N (n+m) = Z.of_N n + Z.of_N m.
+Proof.
+ now destruct n, m.
+Qed.
 
-(** Injection and usual operations *)
+Lemma inj_mul n m : Z.of_N (n*m) = Z.of_N n * Z.of_N m.
+Proof.
+ now destruct n, m.
+Qed.
 
-Theorem inj_plus : forall n m:nat, Z_of_nat (n + m) = Z_of_nat n + Z_of_nat m.
+Lemma inj_sub_max n m : Z.of_N (n-m) = Z.max 0 (Z.of_N n - Z.of_N m).
 Proof.
- induction n as [|n IH]; intros [|m]; simpl; trivial.
- rewrite <- plus_n_O; trivial.
- change (Z_of_nat (S (n + S m)) = Z_of_nat (S n) + Z_of_nat (S m)).
- now rewrite inj_S, IH, 2 inj_S, Zplus_succ_l.
+ destruct n as [|n], m as [|m]; simpl; trivial.
+ rewrite Z.pos_sub_spec, <- Pos.sub_mask_compare. unfold Pos.sub.
+ now destruct (Pos.sub_mask n m).
 Qed.
 
-Theorem inj_mult : forall n m:nat, Z_of_nat (n * m) = Z_of_nat n * Z_of_nat m.
+Lemma inj_sub n m : (m<=n)%N -> Z.of_N (n-m) = Z.of_N n - Z.of_N m.
 Proof.
- induction n as [|n IH]; intros m; trivial.
- rewrite inj_S, Zmult_succ_l, <- IH, <- inj_plus.
- simpl. now rewrite plus_comm.
+ intros H. rewrite inj_sub_max.
+ unfold N.le in H.
+ rewrite <- N.compare_antisym, <- inj_compare, Z.compare_sub in H.
+ destruct (Z.of_N n - Z.of_N m); trivial; now destruct H.
 Qed.
 
-Theorem inj_minus1 :
-  forall n m:nat, (m <= n)%nat -> Z_of_nat (n - m) = Z_of_nat n - Z_of_nat m.
+Lemma inj_succ n : Z.of_N (N.succ n) = Z.succ (Z.of_N n).
 Proof.
- intros n m H.
- apply (Zplus_reg_l (Z_of_nat m)); unfold Zminus.
- rewrite Zplus_permute, Zplus_opp_r, <- inj_plus, Zplus_0_r.
- f_equal. symmetry. now apply le_plus_minus.
+ destruct n. trivial. simpl. now rewrite Pos.add_1_r.
 Qed.
 
-Theorem inj_minus2 : forall n m:nat, (m > n)%nat -> Z_of_nat (n - m) = 0.
+Lemma inj_pred_max n : Z.of_N (N.pred n) = Z.max 0 (Z.pred (Z.of_N n)).
 Proof.
- intros. rewrite not_le_minus_0; auto with arith.
+ unfold Z.pred. now rewrite N.pred_sub, inj_sub_max.
 Qed.
 
-Theorem inj_minus : forall n m:nat,
- Z_of_nat (minus n m) = Zmax 0 (Z_of_nat n - Z_of_nat m).
+Lemma inj_pred n : (0<n)%N -> Z.of_N (N.pred n) = Z.pred (Z.of_N n).
 Proof.
- intros n m. unfold Zmax.
- destruct (le_lt_dec m n) as [H|H].
- (* m <= n *)
- rewrite inj_minus1; trivial.
- apply inj_le, Zle_minus_le_0 in H. revert H. unfold Zle.
- case Zcompare_spec; intuition.
- (* n < m *)
- rewrite inj_minus2; trivial.
- apply inj_lt, Zlt_gt in H.
- apply (Zplus_gt_compat_r _ _ (- Z_of_nat m)) in H.
- rewrite Zplus_opp_r in H.
- unfold Zminus. rewrite H; auto.
+ intros H. unfold Z.pred. rewrite N.pred_sub, inj_sub; trivial.
+ now apply N.le_succ_l in H.
 Qed.
 
-Theorem inj_min : forall n m:nat,
-  Z_of_nat (min n m) = Zmin (Z_of_nat n) (Z_of_nat m).
+Lemma inj_min n m : Z.of_N (N.min n m) = Z.min (Z.of_N n) (Z.of_N m).
 Proof.
- intros n m. unfold Zmin. rewrite inj_compare.
- case nat_compare_spec; intros; f_equal; subst; auto with arith.
+ unfold Z.min, N.min. rewrite inj_compare. now case N.compare.
 Qed.
 
-Theorem inj_max : forall n m:nat,
-  Z_of_nat (max n m) = Zmax (Z_of_nat n) (Z_of_nat m).
+Lemma inj_max n m : Z.of_N (N.max n m) = Z.max (Z.of_N n) (Z.of_N m).
 Proof.
- intros n m. unfold Zmax. rewrite inj_compare.
- case nat_compare_spec; intros; f_equal; subst; auto with arith.
+ unfold Z.max, N.max. rewrite inj_compare.
+ case N.compare_spec; intros; subst; trivial.
 Qed.
 
-(** Composition of injections **)
+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 Z_of_nat_of_P : forall p, Z_of_nat (nat_of_P p) = Zpos p.
+Lemma id n : 0<=n -> Z.of_N (Z.to_N n) = n.
 Proof.
- intros p. destruct (nat_of_P_is_S p) as (n,H). rewrite H.
- simpl. f_equal. rewrite <- (nat_of_P_of_succ_nat n) in H.
- symmetry. now apply nat_of_P_inj.
+ destruct n; (now destruct 1) || trivial.
 Qed.
 
-(** For compatibility *)
-Definition Zpos_eq_Z_of_nat_o_nat_of_P p := eq_sym _ _ _ (Z_of_nat_of_P p).
+(** [Z.to_N] is hence injective for non-negative integers. *)
 
-(******************************************************************)
-(** Properties of the injection from N into Z *)
+Lemma inj n m : 0<=n -> 0<=m -> Z.to_N n = Z.to_N m -> n = m.
+Proof.
+ intros. rewrite <- (id n), <- (id m) by trivial. now f_equal.
+Qed.
 
-Lemma Z_of_nat_of_N : forall n, Z_of_nat (nat_of_N n) = Z_of_N n.
+Lemma inj_iff n m : 0<=n -> 0<=m -> (Z.to_N n = Z.to_N m <-> n = m).
 Proof.
-  intros [|n]. trivial.
-  simpl. apply Z_of_nat_of_P.
+ intros. split. now apply inj. intros; now subst.
 Qed.
 
-Lemma Z_of_N_of_nat : forall n, Z_of_N (N_of_nat n) = Z_of_nat n.
+(** [Z.to_N], basic equations *)
+
+Lemma inj_0 : Z.to_N 0 = 0%N.
 Proof.
- now destruct n.
+ reflexivity.
 Qed.
 
-Lemma Z_of_N_eq : forall n m, n = m -> Z_of_N n = Z_of_N m.
+Lemma inj_pos n : Z.to_N (Zpos n) = Npos n.
 Proof.
- intros; f_equal; assumption.
+ reflexivity.
 Qed.
 
-Lemma Z_of_N_eq_rev : forall n m, Z_of_N n = Z_of_N m -> n = m.
+Lemma inj_neg n : Z.to_N (Zneg n) = 0%N.
 Proof.
- intros [|n] [|m]; simpl; congruence.
+ reflexivity.
 Qed.
 
-Lemma Z_of_N_eq_iff : forall n m, n = m <-> Z_of_N n = Z_of_N m.
+(** [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.
 Proof.
- split; [apply Z_of_N_eq | apply Z_of_N_eq_rev].
+ destruct n, m; trivial; (now destruct 1) || (now destruct 2).
 Qed.
 
-Lemma Z_of_N_compare : forall n m,
- Zcompare (Z_of_N n) (Z_of_N m) = Ncompare n m.
+Lemma inj_mul n m : 0<=n -> 0<=m -> Z.to_N (n*m) = (Z.to_N n * Z.to_N m)%N.
 Proof.
- intros [|n] [|m]; trivial.
+ destruct n, m; trivial; (now destruct 1) || (now destruct 2).
 Qed.
 
-Lemma Z_of_N_le_iff : forall n m, (n<=m)%N <-> Z_of_N n <= Z_of_N m.
+Lemma inj_succ n : 0<=n -> Z.to_N (Z.succ n) = N.succ (Z.to_N n).
 Proof.
- intros. unfold Zle. now rewrite Z_of_N_compare.
+ unfold Z.succ. intros. rewrite inj_add by easy. apply N.add_1_r.
 Qed.
 
-Lemma Z_of_N_le : forall n m, (n<=m)%N -> Z_of_N n <= Z_of_N m.
+Lemma inj_sub n m : 0<=m -> Z.to_N (n - m) = (Z.to_N n - Z.to_N m)%N.
 Proof.
- apply Z_of_N_le_iff.
+ destruct n as [|n|n], m as [|m|m]; trivial; try (now destruct 1).
+ intros _. simpl.
+ rewrite Z.pos_sub_spec, <- Pos.sub_mask_compare. unfold Pos.sub.
+ now destruct (Pos.sub_mask n m).
 Qed.
 
-Lemma Z_of_N_le_rev : forall n m, Z_of_N n <= Z_of_N m -> (n<=m)%N.
+Lemma inj_pred n : Z.to_N (Z.pred n) = N.pred (Z.to_N n).
 Proof.
- apply Z_of_N_le_iff.
+ unfold Z.pred. rewrite <- N.sub_1_r. now apply (inj_sub n 1).
 Qed.
 
-Lemma Z_of_N_lt_iff : forall n m, (n<m)%N <-> Z_of_N n < Z_of_N m.
+Lemma inj_compare n m : 0<=n -> 0<=m ->
+ (Z.to_N n ?= Z.to_N m)%N = (n ?= m).
 Proof.
- intros. unfold Zlt. now rewrite Z_of_N_compare.
+ intros Hn Hm. now rewrite <- N2Z.inj_compare, !id.
 Qed.
 
-Lemma Z_of_N_lt : forall n m, (n<m)%N -> Z_of_N n < Z_of_N m.
+Lemma inj_min n m : Z.to_N (Z.min n m) = N.min (Z.to_N n) (Z.to_N m).
 Proof.
- apply Z_of_N_lt_iff.
+ destruct n, m; simpl; trivial; unfold Z.min, N.min; simpl;
+  now case Pos.compare.
 Qed.
 
-Lemma Z_of_N_lt_rev : forall n m, Z_of_N n < Z_of_N m -> (n<m)%N.
+Lemma inj_max n m : Z.to_N (Z.max n m) = N.max (Z.to_N n) (Z.to_N m).
 Proof.
- apply Z_of_N_lt_iff.
+ destruct n, m; simpl; trivial; unfold Z.max, N.max; simpl.
+  case Pos.compare_spec; intros; subst; trivial.
+  now case Pos.compare.
 Qed.
 
-Lemma Z_of_N_ge_iff : forall n m, (n>=m)%N <-> Z_of_N n >= Z_of_N m.
+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).
 Proof.
- intros. unfold Zge. now rewrite Z_of_N_compare.
+ now destruct n.
 Qed.
 
-Lemma Z_of_N_ge : forall n m, (n>=m)%N -> Z_of_N n >= Z_of_N m.
+Lemma abs_N_nonneg n : 0<=n -> Z.abs_N n = Z.to_N n.
 Proof.
- apply Z_of_N_ge_iff.
+ destruct n; trivial; now destruct 1.
 Qed.
 
-Lemma Z_of_N_ge_rev : forall n m, Z_of_N n >= Z_of_N m -> (n>=m)%N.
+Lemma id_abs n : Z.of_N (Z.abs_N n) = Z.abs n.
 Proof.
- apply Z_of_N_ge_iff.
+ now destruct n.
 Qed.
 
-Lemma Z_of_N_gt_iff : forall n m, (n>m)%N <-> Z_of_N n > Z_of_N m.
+Lemma id n : Z.abs_N (Z.of_N n) = n.
 Proof.
- intros. unfold Zgt. now rewrite Z_of_N_compare.
+ now destruct n.
 Qed.
 
-Lemma Z_of_N_gt : forall n m, (n>m)%N -> Z_of_N n > Z_of_N m.
+(** [Z.abs_N], basic equations *)
+
+Lemma inj_0 : Z.abs_N 0 = 0%N.
 Proof.
- apply Z_of_N_gt_iff.
+ reflexivity.
 Qed.
 
-Lemma Z_of_N_gt_rev : forall n m, Z_of_N n > Z_of_N m -> (n>m)%N.
+Lemma inj_pos p : Z.abs_N (Zpos p) = Npos p.
 Proof.
- apply Z_of_N_gt_iff.
+ reflexivity.
 Qed.
 
-Lemma Z_of_N_pos : forall p:positive, Z_of_N (Npos p) = Zpos p.
+Lemma inj_neg p : Z.abs_N (Zneg p) = Npos p.
 Proof.
  reflexivity.
 Qed.
 
-Lemma Z_of_N_abs : forall z:Z, Z_of_N (Zabs_N z) = Zabs z.
+(** [Z.abs_N] and usual operations, with non-negative integers *)
+
+Lemma inj_succ n : 0<=n -> Z.abs_N (Z.succ n) = N.succ (Z.abs_N n).
 Proof.
- now destruct z.
+ intros. rewrite !abs_N_nonneg; trivial. now apply Z2N.inj_succ.
+ now apply Z.le_le_succ_r.
 Qed.
 
-Lemma Z_of_N_le_0 : forall n, 0 <= Z_of_N n.
+Lemma inj_add n m : 0<=n -> 0<=m -> Z.abs_N (n+m) = (Z.abs_N n + Z.abs_N m)%N.
 Proof.
- now destruct n.
+ intros. rewrite !abs_N_nonneg; trivial. now apply Z2N.inj_add.
+ 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.
+Proof.
+ 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.
+Proof.
+ intros (Hn,H). rewrite !abs_N_nonneg; trivial. now apply Z2N.inj_sub.
+ Z.order.
+ 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).
+Proof.
+ intros. rewrite !abs_N_nonneg. now apply Z2N.inj_pred.
+ Z.order.
+ apply Z.lt_succ_r. 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).
+Proof.
+ intros. rewrite !abs_N_nonneg by trivial. now apply Z2N.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).
+Proof.
+ intros. rewrite !abs_N_nonneg; trivial. now apply Z2N.inj_min.
+ 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).
+Proof.
+ intros. rewrite !abs_N_nonneg; trivial. now apply Z2N.inj_max.
+ transitivity n; trivial. apply Z.le_max_l.
 Qed.
 
-Lemma Z_of_N_plus : forall n m, Z_of_N (n+m) = Z_of_N n + Z_of_N m.
+(** [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).
+Proof.
+ 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.
 Proof.
  now destruct n, m.
 Qed.
 
-Lemma Z_of_N_mult : forall n m, Z_of_N (n*m) = Z_of_N n * Z_of_N m.
+Lemma inj_mul_abs n m :
+ Z.abs_N (Z.abs n * Z.abs m) = (Z.abs_N n * Z.abs_N m)%N.
 Proof.
  now destruct n, m.
 Qed.
 
-Lemma Z_of_N_minus : forall n m, Z_of_N (n-m) = Zmax 0 (Z_of_N n - Z_of_N m).
+End Zabs2N.
+
+
+(** * Conversions between [Z] and [nat] *)
+
+Module Nat2Z.
+
+(** [Z.of_nat], basic equations *)
+
+Lemma inj_0 : Z.of_nat 0 = 0.
+Proof.
+ reflexivity.
+Qed.
+
+Lemma inj_succ n : Z.of_nat (S n) = Z.succ (Z.of_nat n).
+Proof.
+ destruct n. trivial. simpl. symmetry. apply Z.succ_Zpos.
+Qed.
+
+(** [Z.of_N] produce non-negative integers *)
+
+Lemma is_nonneg n : 0 <= Z.of_nat n.
+Proof.
+ 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.
+Proof.
+ 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.
+Proof.
+ intros H. now rewrite <- (id n), <- (id m), H.
+Qed.
+
+Lemma inj_iff n m : Z.of_nat n = Z.of_nat m <-> n = m.
+Proof.
+ split. apply inj. intros; now f_equal.
+Qed.
+
+(** [Z.of_nat] and usual operations *)
+
+Lemma inj_compare n m : (Z.of_nat n ?= Z.of_nat m) = nat_compare n m.
+Proof.
+ 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.
+Proof.
+ unfold Z.le. now rewrite inj_compare, nat_compare_le.
+Qed.
+
+Lemma inj_lt n m : (n<m)%nat <-> Z.of_nat n < Z.of_nat m.
+Proof.
+ unfold Z.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.
+Proof.
+ unfold Z.ge. now rewrite inj_compare, nat_compare_ge.
+Qed.
+
+Lemma inj_gt n m : (n>m)%nat <-> Z.of_nat n > Z.of_nat m.
+Proof.
+ unfold Z.gt. now rewrite inj_compare, nat_compare_gt.
+Qed.
+
+Lemma inj_abs_nat z : Z.of_nat (Z.abs_nat z) = Z.abs z.
+Proof.
+ 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.
+Proof.
+ now rewrite <- !nat_N_Z, Nat2N.inj_add, N2Z.inj_add.
+Qed.
+
+Lemma inj_mul n m : Z.of_nat (n*m) = Z.of_nat n * Z.of_nat m.
+Proof.
+ now rewrite <- !nat_N_Z, Nat2N.inj_mul, N2Z.inj_mul.
+Qed.
+
+Lemma inj_sub_max n m : Z.of_nat (n-m) = Z.max 0 (Z.of_nat n - Z.of_nat m).
+Proof.
+ 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.
+Proof.
+ rewrite nat_compare_le, Nat2N.inj_compare. intros.
+ now rewrite <- !nat_N_Z, Nat2N.inj_sub, N2Z.inj_sub.
+Qed.
+
+Lemma inj_pred_max n : Z.of_nat (pred n) = Z.max 0 (Z.pred (Z.of_nat n)).
+Proof.
+ now rewrite <- !nat_N_Z, Nat2N.inj_pred, N2Z.inj_pred_max.
+Qed.
+
+Lemma inj_pred n : (0<n)%nat -> Z.of_nat (pred n) = Z.pred (Z.of_nat n).
+Proof.
+ rewrite nat_compare_lt, Nat2N.inj_compare. intros.
+ now rewrite <- !nat_N_Z, Nat2N.inj_pred, N2Z.inj_pred.
+Qed.
+
+Lemma inj_min n m : Z.of_nat (min n m) = Z.min (Z.of_nat n) (Z.of_nat m).
+Proof.
+ now rewrite <- !nat_N_Z, Nat2N.inj_min, N2Z.inj_min.
+Qed.
+
+Lemma inj_max n m : Z.of_nat (max n m) = Z.max (Z.of_nat n) (Z.of_nat m).
+Proof.
+ 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.
+Proof.
+ intros. 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.
+Proof.
+ intros. rewrite <- (id n), <- (id m) by trivial. now f_equal.
+Qed.
+
+Lemma inj_iff n m : 0<=n -> 0<=m -> (Z.to_nat n = Z.to_nat m <-> n = m).
+Proof.
+ intros. split. now apply inj. intros; now subst.
+Qed.
+
+(** [Z.to_nat], basic equations *)
+
+Lemma inj_0 : Z.to_nat 0 = O.
+Proof.
+ reflexivity.
+Qed.
+
+Lemma inj_pos n : Z.to_nat (Zpos n) = Pos.to_nat n.
+Proof.
+ reflexivity.
+Qed.
+
+Lemma inj_neg n : Z.to_nat (Zneg n) = O.
+Proof.
+ 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.
+Proof.
+ intros. 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.
+Proof.
+ intros. 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).
+Proof.
+ intros. 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.
 Proof.
- intros [|n] [|m]; simpl; trivial. rewrite Z.pos_sub_spec.
- case Pcompare_spec; intros H.
- subst. now rewrite Pminus_mask_diag.
- rewrite Pminus_mask_Lt; trivial.
- unfold Pminus.
- destruct (Pminus_mask_Gt n m (ZC2 _ _ H)) as (q & -> & _); trivial.
+ intros. now rewrite <- !Z_N_nat, Z2N.inj_sub, N2Nat.inj_sub.
 Qed.
 
-Lemma Z_of_N_succ : forall n, Z_of_N (Nsucc n) = Zsucc (Z_of_N n).
+Lemma inj_pred n : Z.to_nat (Z.pred n) = pred (Z.to_nat n).
 Proof.
- intros [|n]; simpl; trivial. now rewrite Zpos_succ_morphism.
+ now rewrite <- !Z_N_nat, Z2N.inj_pred, N2Nat.inj_pred.
 Qed.
 
-Lemma Z_of_N_min : forall n m, Z_of_N (Nmin n m) = Zmin (Z_of_N n) (Z_of_N m).
+Lemma inj_compare n m : 0<=n -> 0<=m ->
+ nat_compare (Z.to_nat n) (Z.to_nat m) = (n ?= m).
 Proof.
- intros. unfold Zmin, Nmin. rewrite Z_of_N_compare. now case Ncompare.
+ intros Hn Hm. now rewrite <- Nat2Z.inj_compare, !id.
 Qed.
 
-Lemma Z_of_N_max : forall n m, Z_of_N (Nmax n m) = Zmax (Z_of_N n) (Z_of_N m).
+Lemma inj_min n m : Z.to_nat (Z.min n m) = min (Z.to_nat n) (Z.to_nat m).
 Proof.
- intros. unfold Zmax, Nmax. rewrite Z_of_N_compare.
- case Ncompare_spec; intros; subst; trivial.
+ now rewrite <- !Z_N_nat, Z2N.inj_min, N2Nat.inj_min.
 Qed.
 
-(** Results about the [Zabs_N] function, converting from Z to N *)
+Lemma inj_max n m : Z.to_nat (Z.max n m) = max (Z.to_nat n) (Z.to_nat m).
+Proof.
+ now rewrite <- !Z_N_nat, Z2N.inj_max, N2Nat.inj_max.
+Qed.
+
+End Z2Nat.
+
+Module Zabs2Nat.
 
-Lemma Zabs_of_N : forall n, Zabs_N (Z_of_N n) = n.
+(** 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).
 Proof.
  now destruct n.
 Qed.
 
-Lemma Zabs_N_succ_abs : forall n,
- Zabs_N (Zsucc (Zabs n)) = Nsucc (Zabs_N n).
+Lemma abs_nat_nonneg n : 0<=n -> Z.abs_nat n = Z.to_nat n.
+Proof.
+ destruct n; trivial; now destruct 1.
+Qed.
+
+Lemma id_abs n : Z.of_nat (Z.abs_nat n) = Z.abs n.
 Proof.
- intros [ |n|n]; simpl; trivial; now rewrite Pplus_one_succ_r.
+ rewrite <-Zabs_N_nat, N_nat_Z. apply Zabs2N.id_abs.
 Qed.
 
-Lemma Zabs_N_succ : forall n, 0<=n ->
- Zabs_N (Zsucc n) = Nsucc (Zabs_N n).
+Lemma id n : Z.abs_nat (Z.of_nat n) = n.
 Proof.
- intros n Hn. rewrite <- Zabs_N_succ_abs. repeat f_equal.
- symmetry; now apply Zabs_eq.
+ now rewrite <-Zabs_N_nat, <-nat_N_Z, Zabs2N.id, Nat2N.id.
 Qed.
 
-Lemma Zabs_N_plus_abs : forall n m,
- Zabs_N (Zabs n + Zabs m) = (Zabs_N n + Zabs_N m)%N.
+(** [Z.abs_nat], basic equations *)
+
+Lemma inj_0 : Z.abs_nat 0 = 0%nat.
+Proof.
+ reflexivity.
+Qed.
+
+Lemma inj_pos p : Z.abs_nat (Zpos p) = Pos.to_nat p.
+Proof.
+ reflexivity.
+Qed.
+
+Lemma inj_neg p : Z.abs_nat (Zneg p) = Pos.to_nat p.
+Proof.
+ 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).
 Proof.
- intros [ |n|n] [ |m|m]; simpl; trivial.
+ intros. now rewrite <- !Zabs_N_nat, Zabs2N.inj_succ, N2Nat.inj_succ.
 Qed.
 
-Lemma Zabs_N_plus : forall n m, 0<=n -> 0<=m ->
- Zabs_N (n + m) = (Zabs_N n + Zabs_N m)%N.
+Lemma inj_add n m : 0<=n -> 0<=m ->
+ Z.abs_nat (n+m) = (Z.abs_nat n + Z.abs_nat m)%nat.
 Proof.
- intros n m Hn Hm.
- rewrite <- Zabs_N_plus_abs; repeat f_equal;
-  symmetry; now apply Zabs_eq.
+ intros. now rewrite <- !Zabs_N_nat, Zabs2N.inj_add, N2Nat.inj_add.
 Qed.
 
-Lemma Zabs_N_mult_abs : forall n m,
- Zabs_N (Zabs n * Zabs m) = (Zabs_N n * Zabs_N m)%N.
+Lemma inj_mul n m : Z.abs_nat (n*m) = (Z.abs_nat n * Z.abs_nat m)%nat.
 Proof.
- intros [ |n|n] [ |m|m]; simpl; trivial.
+ destruct n, m; simpl; trivial using Pos2Nat.inj_mul.
 Qed.
 
-Lemma Zabs_N_mult : forall n m, 0<=n -> 0<=m ->
- Zabs_N (n * m) = (Zabs_N n * Zabs_N m)%N.
+Lemma inj_sub n m : 0<=m<=n ->
+ Z.abs_nat (n-m) = (Z.abs_nat n - Z.abs_nat m)%nat.
 Proof.
- intros n m Hn Hm.
- rewrite <- Zabs_N_mult_abs; repeat f_equal;
-  symmetry; now apply Zabs_eq.
+ intros. now rewrite <- !Zabs_N_nat, Zabs2N.inj_sub, N2Nat.inj_sub.
+Qed.
+
+Lemma inj_pred n : 0<n -> Z.abs_nat (Z.pred n) = pred (Z.abs_nat n).
+Proof.
+ intros. now rewrite <- !Zabs_N_nat, Zabs2N.inj_pred, N2Nat.inj_pred.
+Qed.
+
+Lemma inj_compare n m : 0<=n -> 0<=m ->
+ nat_compare (Z.abs_nat n) (Z.abs_nat m) = (n ?= m).
+Proof.
+ intros. now rewrite <- !Zabs_N_nat, <- N2Nat.inj_compare, Zabs2N.inj_compare.
+Qed.
+
+Lemma inj_min n m : 0<=n -> 0<=m ->
+ Z.abs_nat (Z.min n m) = min (Z.abs_nat n) (Z.abs_nat m).
+Proof.
+ intros. 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) = max (Z.abs_nat n) (Z.abs_nat m).
+Proof.
+ intros. 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).
+Proof.
+ 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.
+Proof.
+ 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.
+Proof.
+ 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).
+Proof. intros H H'. now apply H, Nat2Z.inj. Qed.
+
+Lemma Zpos_P_of_succ_nat n : Zpos (P_of_succ_nat n) = Zsucc (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).
+
+(** 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 => sym_eq (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.
+Proof.
+ intros. rewrite not_le_minus_0; auto with arith.
 Qed.