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

1 files changed, 627 insertions, 190 deletions

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.