22 files changed, 1266 insertions, 102 deletions

diff --git a/contrib/omega/Omega.v b/contrib/omega/Omega.v
index 3bc5a32e3c..3b427162e8 100644
--- a/contrib/omega/Omega.v
+++ b/contrib/omega/Omega.v
@@ -9,7 +9,7 @@
 (*                                                                        *)
 (* Omega: a solver of quantifier-free problems in Presburger Arithmetic   *)
 (*                                                                        *)
-(* Pierre Crégut (CNET, Lannion, France)                                  *)
+(* Pierre Crégut (CNET, Lannion, France)                                  *)
 (*                                                                        *)
 (**************************************************************************)
 
@@ -18,6 +18,7 @@
 (* We do not require [ZArith] anymore, but only what's necessary for Omega *)
 Require Export ZArith_base.
 Require Export OmegaLemmas.
+Require Export PreOmega.
 
 Hint Resolve Zle_refl Zplus_comm Zplus_assoc Zmult_comm Zmult_assoc Zplus_0_l
   Zplus_0_r Zmult_1_l Zplus_opp_l Zplus_opp_r Zmult_plus_distr_l
diff --git a/contrib/omega/PreOmega.v b/contrib/omega/PreOmega.v
new file mode 100644
index 0000000000..0a43284978
--- /dev/null
+++ b/contrib/omega/PreOmega.v
@@ -0,0 +1,445 @@
+Require Import Arith Max Min ZArith_base NArith Nnat.
+
+Open Local Scope Z_scope.
+
+
+(** * zify: the Z-ification tactic *)
+
+(* This tactic searches for nat and N and positive elements in the goal and 
+   translates everything into Z. It is meant as a pre-processor for 
+   (r)omega; for instance a positivity hypothesis is added whenever
+     - a multiplication is encountered
+     - an atom is encountered (that is a variable or an unknown construct)
+
+   Recognized relations (can be handled as deeply as allowed by setoid rewrite):
+     - { eq, le, lt, ge, gt } on { Z, positive, N, nat }
+   
+   Recognized operations: 
+     - on Z: Zmin, Zmax, Zabs, Zsgn are translated in term of <= < =
+     - on nat: + * - S O pred min max nat_of_P nat_of_N Zabs_nat
+     - on positive: Zneg Zpos xI xO xH + * - Psucc Ppred Pmin Pmax P_of_succ_nat
+     - on N: N0 Npos + * - Nsucc Nmin Nmax N_of_nat Zabs_N
+*)
+
+
+
+
+(** I) translation of Zmax, Zmin, Zabs, Zsgn into recognized equations *)
+
+Ltac zify_unop_core t thm a := 
+ (* Let's introduce the specification theorem for t *)
+ let H:= fresh "H" in assert (H:=thm a); 
+ (* Then we replace (t a) everywhere with a fresh variable *)
+ let z := fresh "z" in set (z:=t a) in *; clearbody z.
+
+Ltac zify_unop_var_or_term t thm a := 
+ (* If a is a variable, no need for aliasing *)
+ let za := fresh "z" in 
+ (rename a into za; rename za into a; zify_unop_core t thm a) ||
+ (* Otherwise, a is a complex term: we alias it. *)
+ (remember a as za; zify_unop_core t thm za).
+
+Ltac zify_unop t thm a := 
+ (* if a is a scalar, we can simply reduce the unop *)
+ let isz := isZcst a in 
+ match isz with 
+  | true => simpl (t a) in *
+  | _ => zify_unop_var_or_term t thm a
+ end.
+
+Ltac zify_unop_nored t thm a := 
+ (* in this version, we don't try to reduce the unop (that can be (Zplus x)) *)
+ let isz := isZcst a in 
+ match isz with 
+  | true => zify_unop_core t thm a
+  | _ => zify_unop_var_or_term t thm a
+ end.
+
+Ltac zify_binop t thm a b:=
+ (* works as zify_unop, except that we should be careful when
+    dealing with b, since it can be equal to a *)
+ let isza := isZcst a in 
+ match isza with 
+   | true => zify_unop (t a) (thm a) b
+   | _ => 
+       let za := fresh "z" in 
+       (rename a into za; rename za into a; zify_unop_nored (t a) (thm a) b) ||
+       (remember a as za; match goal with 
+         | H : za = b |- _ => zify_unop_nored (t za) (thm za) za
+         | _ => zify_unop_nored (t za) (thm za) b
+        end)
+ end.
+
+Ltac zify_op_1 := 
+  match goal with 
+   | |- context [ Zmax ?a ?b ] => zify_binop Zmax Zmax_spec a b
+   | H : context [ Zmax ?a ?b ] |- _ => zify_binop Zmax Zmax_spec a b
+   | |- context [ Zmin ?a ?b ] => zify_binop Zmin Zmin_spec a b
+   | H : context [ Zmin ?a ?b ] |- _ => zify_binop Zmin Zmin_spec a b
+   | |- context [ Zsgn ?a ] => zify_unop Zsgn Zsgn_spec a
+   | H : context [ Zsgn ?a ] |- _ => zify_unop Zsgn Zsgn_spec a
+   | |- context [ Zabs ?a ] => zify_unop Zabs Zabs_spec a
+   | H : context [ Zabs ?a ] |- _ => zify_unop Zabs Zabs_spec a
+  end.
+
+Ltac zify_op := repeat zify_op_1.
+
+
+
+
+
+(** II) Conversion from nat to Z *)
+
+
+Definition Z_of_nat' := Z_of_nat.
+
+Ltac hide_Z_of_nat t := 
+  let z := fresh "z" in set (z:=Z_of_nat t) in *; 
+  change Z_of_nat with Z_of_nat' in z; 
+  unfold z in *; clear z.
+
+Ltac zify_nat_rel := 
+ match goal with 
+  (* I: equalities *)
+  | H : (@eq nat ?a ?b) |- _ => generalize (inj_eq _ _ H); clear H; intro H
+  | |- (@eq nat ?a ?b) => apply (inj_eq_rev a b)
+  | H : context [ @eq nat ?a ?b ] |- _ => rewrite (inj_eq_iff a b) in H
+  | |- context [ @eq nat ?a ?b ] =>       rewrite (inj_eq_iff a b)
+  (* II: less than *)
+  | H : (lt ?a ?b) |- _ => generalize (inj_lt _ _ H); clear H; intro H
+  | |- (lt ?a ?b) => apply (inj_lt_rev a b)
+  | H : context [ lt ?a ?b ] |- _ => rewrite (inj_lt_iff a b) in H
+  | |- context [ lt ?a ?b ] =>       rewrite (inj_lt_iff a b)
+  (* III: less or equal *)
+  | H : (le ?a ?b) |- _ => generalize (inj_le _ _ H); clear H; intro H
+  | |- (le ?a ?b) => apply (inj_le_rev a b)
+  | H : context [ le ?a ?b ] |- _ => rewrite (inj_le_iff a b) in H
+  | |- context [ le ?a ?b ] =>       rewrite (inj_le_iff a b)
+  (* IV: greater than *)
+  | H : (gt ?a ?b) |- _ => generalize (inj_gt _ _ H); clear H; intro H
+  | |- (gt ?a ?b) => apply (inj_gt_rev a b)
+  | H : context [ gt ?a ?b ] |- _ => rewrite (inj_gt_iff a b) in H
+  | |- context [ gt ?a ?b ] =>       rewrite (inj_gt_iff a b)
+  (* V: greater or equal *)
+  | H : (ge ?a ?b) |- _ => generalize (inj_ge _ _ H); clear H; intro H
+  | |- (ge ?a ?b) => apply (inj_ge_rev a b)
+  | H : context [ ge ?a ?b ] |- _ => rewrite (inj_ge_iff a b) in H
+  | |- context [ ge ?a ?b ] =>       rewrite (inj_ge_iff a b)
+ end.
+
+Ltac zify_nat_op := 
+ match goal with 
+  (* misc type conversions: positive/N/Z to nat *)
+  | H : context [ Z_of_nat (nat_of_P ?a) ] |- _ => rewrite <- (Zpos_eq_Z_of_nat_o_nat_of_P a) in H
+  | |- context [ Z_of_nat (nat_of_P ?a) ] => rewrite <- (Zpos_eq_Z_of_nat_o_nat_of_P a)
+  | H : context [ Z_of_nat (nat_of_N ?a) ] |- _ => rewrite (Z_of_nat_of_N a) in H
+  | |- context [ Z_of_nat (nat_of_N ?a) ] => rewrite (Z_of_nat_of_N a)
+  | H : context [ Z_of_nat (Zabs_nat ?a) ] |- _ => rewrite (inj_Zabs_nat a) in H
+  | |- context [ Z_of_nat (Zabs_nat ?a) ] => rewrite (inj_Zabs_nat a)
+
+  (* plus -> Zplus *)
+  | H : context [ Z_of_nat (plus ?a ?b) ] |- _ => rewrite (inj_plus a b) in H
+  | |- context [ Z_of_nat (plus ?a ?b) ] => rewrite (inj_plus a b)
+
+  (* min -> Zmin *)
+  | H : context [ Z_of_nat (min ?a ?b) ] |- _ => rewrite (inj_min a b) in H
+  | |- context [ Z_of_nat (min ?a ?b) ] => rewrite (inj_min a b)
+
+  (* max -> Zmax *)
+  | H : context [ Z_of_nat (max ?a ?b) ] |- _ => rewrite (inj_max a b) in H
+  | |- context [ Z_of_nat (max ?a ?b) ] => rewrite (inj_max a b)
+
+  (* minus -> Zmax (Zminus ... ...) 0 *)
+  | H : context [ Z_of_nat (minus ?a ?b) ] |- _ => rewrite (inj_minus a b) in H
+  | |- context [ Z_of_nat (minus ?a ?b) ] => rewrite (inj_minus a b)
+
+  (* pred -> minus ... -1 -> Zmax (Zminus ... -1) 0 *)
+  | H : context [ Z_of_nat (pred ?a) ] |- _ => rewrite (pred_of_minus a) in H
+  | |- context [ Z_of_nat (pred ?a) ] => rewrite (pred_of_minus a)
+
+  (* mult -> Zmult and a positivity hypothesis *)
+  | H : context [ Z_of_nat (mult ?a ?b) ] |- _ => 
+        let H:= fresh "H" in 
+        assert (H:=Zle_0_nat (mult a b)); rewrite (inj_mult a b) in *
+  | |- context [ Z_of_nat (mult ?a ?b) ] => 
+        let H:= fresh "H" in 
+        assert (H:=Zle_0_nat (mult a b)); rewrite (inj_mult a b) in *
+
+  (* O -> Z0 *)
+  | H : context [ Z_of_nat O ] |- _ => simpl (Z_of_nat O) in H
+  | |- context [ Z_of_nat O ] => simpl (Z_of_nat O)
+
+  (* S -> number or Zsucc *)
+  | H : context [ Z_of_nat (S ?a) ] |- _ => 
+     let isnat := isnatcst a in 
+     match isnat with 
+      | true => simpl (Z_of_nat (S a)) in H
+      | _ => rewrite (inj_S a) in H
+     end
+  | |- context [ Z_of_nat (S ?a) ] => 
+     let isnat := isnatcst a in 
+     match isnat with 
+      | true => simpl (Z_of_nat (S a))
+      | _ => rewrite (inj_S a)
+     end
+
+  (* atoms of type nat : we add a positivity condition (if not already there) *) 
+  | H : context [ Z_of_nat ?a ] |- _ => 
+        match goal with 
+          | H' : 0 <= Z_of_nat a |- _ => hide_Z_of_nat a
+          | H' : 0 <= Z_of_nat' a |- _ => fail
+          | _ => let H:= fresh "H" in
+                 assert (H:=Zle_0_nat a); hide_Z_of_nat a
+        end
+  | |- context [ Z_of_nat ?a ] => 
+        match goal with 
+          | H' : 0 <= Z_of_nat a |- _ => hide_Z_of_nat a
+          | H' : 0 <= Z_of_nat' a |- _ => fail
+          | _ => let H:= fresh "H" in
+                 assert (H:=Zle_0_nat a); hide_Z_of_nat a
+        end
+ end.
+
+Ltac zify_nat := repeat zify_nat_rel; repeat zify_nat_op; unfold Z_of_nat' in *.
+
+
+
+
+(* III) conversion from positive to Z *) 
+
+Definition Zpos' := Zpos.
+Definition Zneg' := Zneg.
+
+Ltac hide_Zpos t := 
+  let z := fresh "z" in set (z:=Zpos t) in *; 
+  change Zpos with Zpos' in z; 
+  unfold z in *; clear z.
+
+Ltac zify_positive_rel := 
+ match goal with 
+  (* I: equalities *)
+  | H : (@eq positive ?a ?b) |- _ => generalize (Zpos_eq _ _ H); clear H; intro H
+  | |- (@eq positive ?a ?b) => apply (Zpos_eq_rev a b)
+  | H : context [ @eq positive ?a ?b ] |- _ => rewrite (Zpos_eq_iff a b) in H
+  | |- context [ @eq positive ?a ?b ] =>       rewrite (Zpos_eq_iff a b)
+  (* II: less than *)
+  | H : context [ (?a<?b)%positive ] |- _ => change (a<b)%positive with (Zpos a<Zpos b) in H
+  | |- context [ (?a<?b)%positive ] => change (a<b)%positive with (Zpos a<Zpos b)
+  (* III: less or equal *)
+  | H : context [ (?a<=?b)%positive ] |- _ => change (a<=b)%positive with (Zpos a<=Zpos b) in H
+  | |- context [ (?a<=?b)%positive ] => change (a<=b)%positive with (Zpos a<=Zpos b)
+  (* IV: greater than *)
+  | H : context [ (?a>?b)%positive ] |- _ => change (a>b)%positive with (Zpos a>Zpos b) in H
+  | |- context [ (?a>?b)%positive ] => change (a>b)%positive with (Zpos a>Zpos b)
+  (* V: greater or equal *)
+  | H : context [ (?a>=?b)%positive ] |- _ => change (a>=b)%positive with (Zpos a>=Zpos b) in H
+  | |- context [ (?a>=?b)%positive ] => change (a>=b)%positive with (Zpos a>=Zpos b)
+ end.
+
+Ltac zify_positive_op := 
+ match goal with 
+  (* Zneg -> -Zpos (except for numbers) *)
+  | H : context [ Zneg ?a ] |- _ => 
+     let isp := isPcst a in 
+     match isp with 
+      | true => change (Zneg a) with (Zneg' a) in H
+      | _ => change (Zneg a) with (- Zpos a) in H
+     end
+  | |- context [ Zneg ?a ] => 
+     let isp := isPcst a in 
+     match isp with 
+      | true => change (Zneg a) with (Zneg' a)
+      | _ => change (Zneg a) with (- Zpos a)
+     end
+
+  (* misc type conversions: nat to positive *)
+  | H : context [ Zpos (P_of_succ_nat ?a) ] |- _ => rewrite (Zpos_P_of_succ_nat a) in H
+  | |- context [ Zpos (P_of_succ_nat ?a) ] => rewrite (Zpos_P_of_succ_nat a)
+
+  (* Pplus -> Zplus *)
+  | H : context [ Zpos (Pplus ?a ?b) ] |- _ => change (Zpos (Pplus a b)) with (Zplus (Zpos a) (Zpos b)) in H
+  | |- context [ Zpos (Pplus ?a ?b) ] => change (Zpos (Pplus a b)) with (Zplus (Zpos a) (Zpos b))
+
+  (* Pmin -> Zmin *)
+  | H : context [ Zpos (Pmin ?a ?b) ] |- _ => rewrite (Zpos_min a b) in H
+  | |- context [ Zpos (Pmin ?a ?b) ] => rewrite (Zpos_min a b)
+
+  (* Pmax -> Zmax *)
+  | H : context [ Zpos (Pmax ?a ?b) ] |- _ => rewrite (Zpos_max a b) in H
+  | |- context [ Zpos (Pmax ?a ?b) ] => rewrite (Zpos_max a b)
+
+  (* Pminus -> Zmax 1 (Zminus ... ...) *)
+  | H : context [ Zpos (Pminus ?a ?b) ] |- _ => rewrite (Zpos_minus a b) in H
+  | |- context [ Zpos (Pminus ?a ?b) ] => rewrite (Zpos_minus a b)
+
+  (* Psucc -> Zsucc *) 
+  | H : context [ Zpos (Psucc ?a) ] |- _ => rewrite (Zpos_succ_morphism a) in H
+  | |- context [ Zpos (Psucc ?a) ] => rewrite (Zpos_succ_morphism a)
+
+  (* Ppred -> Pminus ... -1 -> Zmax 1 (Zminus ... - 1) *)
+  | H : context [ Zpos (Ppred ?a) ] |- _ => rewrite (Ppred_minus a) in H
+  | |- context [ Zpos (Ppred ?a) ] => rewrite (Ppred_minus a)
+ 
+  (* Pmult -> Zmult and a positivity hypothesis *)
+  | H : context [ Zpos (Pmult ?a ?b) ] |- _ => 
+        let H:= fresh "H" in 
+        assert (H:=Zgt_pos_0 (Pmult a b)); rewrite (Zpos_mult_morphism a b) in *
+  | |- context [ Zpos (Pmult ?a ?b) ] => 
+        let H:= fresh "H" in 
+        assert (H:=Zgt_pos_0 (Pmult a b)); rewrite (Zpos_mult_morphism a b) in *
+
+  (* xO *)
+  | H : context [ Zpos (xO ?a) ] |- _ => 
+     let isp := isPcst a in 
+     match isp with 
+      | true => change (Zpos (xO a)) with (Zpos' (xO a)) in H
+      | _ => rewrite (Zpos_xO a) in H
+     end
+  | |- context [ Zpos (xO ?a) ] => 
+     let isp := isPcst a in 
+     match isp with 
+      | true => change (Zpos (xO a)) with (Zpos' (xO a))
+      | _ => rewrite (Zpos_xO a)
+     end
+  (* xI *) 
+  | H : context [ Zpos (xI ?a) ] |- _ => 
+     let isp := isPcst a in 
+     match isp with 
+      | true => change (Zpos (xI a)) with (Zpos' (xI a)) in H
+      | _ => rewrite (Zpos_xI a) in H
+     end
+  | |- context [ Zpos (xI ?a) ] => 
+     let isp := isPcst a in 
+     match isp with 
+      | true => change (Zpos (xI a)) with (Zpos' (xI a))
+      | _ => rewrite (Zpos_xI a)
+     end
+
+  (* xI : nothing to do, just prevent adding a useless positivity condition *)
+  | H : context [ Zpos xH ] |- _ => hide_Zpos xH
+  | |- context [ Zpos xH ] => hide_Zpos xH
+
+  (* atoms of type positive : we add a positivity condition (if not already there) *)
+  | H : context [ Zpos ?a ] |- _ => 
+        match goal with 
+         | H' : Zpos a > 0 |- _ => hide_Zpos a
+         | H' : Zpos' a > 0 |- _ => fail
+         | _ => let H:= fresh "H" in assert (H:=Zgt_pos_0 a); hide_Zpos a
+        end
+  | |- context [ Zpos ?a ] => 
+        match goal with 
+         | H' : Zpos a > 0 |- _ => hide_Zpos a
+         | H' : Zpos' a > 0 |- _ => fail
+         | _ => let H:= fresh "H" in assert (H:=Zgt_pos_0 a); hide_Zpos a
+        end
+ end.
+
+Ltac zify_positive := 
+ repeat zify_positive_rel; repeat zify_positive_op; unfold Zpos',Zneg' in *.
+
+
+
+
+
+(* IV) conversion from N to Z *) 
+
+Definition Z_of_N' := Z_of_N.
+
+Ltac hide_Z_of_N t := 
+  let z := fresh "z" in set (z:=Z_of_N t) in *; 
+  change Z_of_N with Z_of_N' in z; 
+  unfold z in *; clear z.
+
+Ltac zify_N_rel := 
+ match goal with 
+  (* I: equalities *)
+  | H : (@eq N ?a ?b) |- _ => generalize (Z_of_N_eq _ _ H); clear H; intro H
+  | |- (@eq N ?a ?b) => apply (Z_of_N_eq_rev a b)
+  | H : context [ @eq N ?a ?b ] |- _ => rewrite (Z_of_N_eq_iff a b) in H
+  | |- context [ @eq N ?a ?b ] =>       rewrite (Z_of_N_eq_iff a b)
+  (* II: less than *)
+  | H : (?a<?b)%N |- _ => generalize (Z_of_N_lt _ _ H); clear H; intro H
+  | |- (?a<?b)%N => apply (Z_of_N_lt_rev a b)
+  | H : context [ (?a<?b)%N ] |- _ => rewrite (Z_of_N_lt_iff a b) in H
+  | |- context [ (?a<?b)%N ] =>       rewrite (Z_of_N_lt_iff a b)
+  (* III: less or equal *)
+  | H : (?a<=?b)%N |- _ => generalize (Z_of_N_le _ _ H); clear H; intro H
+  | |- (?a<=?b)%N => apply (Z_of_N_le_rev a b)
+  | H : context [ (?a<=?b)%N ] |- _ => rewrite (Z_of_N_le_iff a b) in H
+  | |- context [ (?a<=?b)%N ] =>       rewrite (Z_of_N_le_iff a b)
+  (* IV: greater than *)
+  | H : (?a>?b)%N |- _ => generalize (Z_of_N_gt _ _ H); clear H; intro H
+  | |- (?a>?b)%N => apply (Z_of_N_gt_rev a b)
+  | H : context [ (?a>?b)%N ] |- _ => rewrite (Z_of_N_gt_iff a b) in H
+  | |- context [ (?a>?b)%N ] =>       rewrite (Z_of_N_gt_iff a b)
+  (* V: greater or equal *)
+  | H : (?a>=?b)%N |- _ => generalize (Z_of_N_ge _ _ H); clear H; intro H
+  | |- (?a>=?b)%N => apply (Z_of_N_ge_rev a b)
+  | H : context [ (?a>=?b)%N ] |- _ => rewrite (Z_of_N_ge_iff a b) in H
+  | |- context [ (?a>=?b)%N ] =>       rewrite (Z_of_N_ge_iff a b)
+ end.
+ 
+Ltac zify_N_op := 
+ match goal with 
+  (* misc type conversions: nat to positive *)
+  | H : context [ Z_of_N (N_of_nat ?a) ] |- _ => rewrite (Z_of_N_of_nat a) in H
+  | |- context [ Z_of_N (N_of_nat ?a) ] => rewrite (Z_of_N_of_nat a)
+  | H : context [ Z_of_N (Zabs_N ?a) ] |- _ => rewrite (Z_of_N_abs a) in H
+  | |- context [ Z_of_N (Zabs_N ?a) ] => rewrite (Z_of_N_abs a)
+  | H : context [ Z_of_N (Npos ?a) ] |- _ => rewrite (Z_of_N_pos a) in H
+  | |- context [ Z_of_N (Npos ?a) ] => rewrite (Z_of_N_pos a)
+  | H : context [ Z_of_N N0 ] |- _ => change (Z_of_N N0) with Z0 in H
+  | |- context [ Z_of_N N0 ] => change (Z_of_N N0) with Z0
+
+  (* Nplus -> Zplus *)
+  | H : context [ Z_of_N (Nplus ?a ?b) ] |- _ => rewrite (Z_of_N_plus a b) in H
+  | |- context [ Z_of_N (Nplus ?a ?b) ] => rewrite (Z_of_N_plus a b)
+
+  (* Nmin -> Zmin *)
+  | H : context [ Z_of_N (Nmin ?a ?b) ] |- _ => rewrite (Z_of_N_min a b) in H
+  | |- context [ Z_of_N (Nmin ?a ?b) ] => rewrite (Z_of_N_min a b)
+
+  (* Nmax -> Zmax *)
+  | H : context [ Z_of_N (Nmax ?a ?b) ] |- _ => rewrite (Z_of_N_max a b) in H
+  | |- context [ Z_of_N (Nmax ?a ?b) ] => rewrite (Z_of_N_max a b)
+
+  (* Nminus -> Zmax 0 (Zminus ... ...) *)
+  | H : context [ Z_of_N (Nminus ?a ?b) ] |- _ => rewrite (Z_of_N_minus a b) in H
+  | |- context [ Z_of_N (Nminus ?a ?b) ] => rewrite (Z_of_N_minus a b)
+
+  (* Nsucc -> Zsucc *) 
+  | H : context [ Z_of_N (Nsucc ?a) ] |- _ => rewrite (Z_of_N_succ a) in H
+  | |- context [ Z_of_N (Nsucc ?a) ] => rewrite (Z_of_N_succ a)
+ 
+  (* Nmult -> Zmult and a positivity hypothesis *)
+  | H : context [ Z_of_N (Pmult ?a ?b) ] |- _ => 
+        let H:= fresh "H" in 
+        assert (H:=Z_of_N_le_0 (Pmult a b)); rewrite (Z_of_N_mult a b) in *
+  | |- context [ Z_of_N  (Pmult ?a ?b) ] => 
+        let H:= fresh "H" in 
+        assert (H:=Z_of_N_le_0 (Pmult a b)); rewrite (Z_of_N_mult a b) in *
+
+  (* atoms of type N : we add a positivity condition (if not already there) *) 
+  | H : context [ Z_of_N ?a ] |- _ => 
+        match goal with 
+         | H' : 0 <= Z_of_N a |- _ => hide_Z_of_N a
+         | H' : 0 <= Z_of_N' a |- _ => fail
+         | _ => let H:= fresh "H" in assert (H:=Z_of_N_le_0 a); hide_Z_of_N a
+        end
+  | |- context [ Z_of_N ?a ] => 
+        match goal with 
+         | H' : 0 <= Z_of_N a |- _ => hide_Z_of_N a
+         | H' : 0 <= Z_of_N' a |- _ => fail
+         | _ => let H:= fresh "H" in assert (H:=Z_of_N_le_0 a); hide_Z_of_N a
+        end
+ end.
+
+Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *.
+
+
+
+(** The complete Z-ification tactic *)
+
+Ltac zify := 
+ repeat progress (zify_nat; zify_positive; zify_N); zify_op.
+
diff --git a/contrib/omega/g_omega.ml4 b/contrib/omega/g_omega.ml4
index 910f110835..a69f8ef745 100644
--- a/contrib/omega/g_omega.ml4
+++ b/contrib/omega/g_omega.ml4
@@ -18,7 +18,30 @@
 (* $Id$ *)
 
 open Coq_omega
+open Refiner
+
+let omega_tactic l = 
+  let tacs = List.map 
+    (function  
+       | "nat" -> Tacinterp.interp <:tactic<zify_nat>>
+       | "positive" -> Tacinterp.interp <:tactic<zify_positive>>
+       | "N" -> Tacinterp.interp <:tactic<zify_N>>
+       | "Z" -> Tacinterp.interp <:tactic<zify_op>>
+       | s -> Util.error ("No Omega knowledge base for type "^s))
+    (Util.list_uniquize (List.sort compare l))
+  in 
+  tclTHEN
+    (tclREPEAT (tclPROGRESS (tclTHENLIST tacs)))
+    omega_solver
+
 
 TACTIC EXTEND omega
-  [ "omega" ] -> [ omega_solver ]
+|  [ "omega" ] -> [ omega_tactic [] ]
 END
+
+TACTIC EXTEND omega'
+| [ "omega" "with" ne_ident_list(l) ] -> 
+    [ omega_tactic (List.map Names.string_of_id l) ]
+| [ "omega" "with" "*" ] -> [ omega_tactic ["nat";"positive";"N";"Z"] ]
+END
+
diff --git a/contrib/romega/ROmega.v b/contrib/romega/ROmega.v
index 19933873be..991267ee5b 100644
--- a/contrib/romega/ROmega.v
+++ b/contrib/romega/ROmega.v
@@ -1,10 +1,10 @@
 (*************************************************************************
 
    PROJET RNRT Calife - 2001
-   Author: Pierre Crégut - France Télécom R&D
+   Author: Pierre Crégut - France Télécom R&D
    Licence : LGPL version 2.1
 
  *************************************************************************)
 
 Require Import ReflOmegaCore.
-
+Require Export PreOmega.
diff --git a/contrib/romega/const_omega.ml b/contrib/romega/const_omega.ml
index 6303605db3..bdec6bf457 100644
--- a/contrib/romega/const_omega.ml
+++ b/contrib/romega/const_omega.ml
@@ -321,6 +321,7 @@ let parse_term t =
     | Kapp("Zmult",[t1;t2]) -> Tmult (t1,t2)
     | Kapp("Zopp",[t]) -> Topp t
     | Kapp("Zsucc",[t]) -> Tsucc t
+    | Kapp("Zpred",[t]) -> Tplus(t, mk_Z (Bigint.neg Bigint.one))
     | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> 
 	(try Tnum (recognize t) with _ -> Tother)
     | _ -> Tother
@@ -341,7 +342,7 @@ let parse_rel gl t =
 let is_scalar t =
   let rec aux t = match destructurate t with
     | Kapp(("Zplus"|"Zminus"|"Zmult"),[t1;t2]) -> aux t1 & aux t2
-    | Kapp(("Zopp"|"Zsucc"),[t]) -> aux t
+    | Kapp(("Zopp"|"Zsucc"|"Zpred"),[t]) -> aux t
     | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> let _ = recognize t in true
     | _ -> false in
   try aux t with _ -> false
diff --git a/contrib/romega/g_romega.ml4 b/contrib/romega/g_romega.ml4
index 7cfc50f8eb..39b6c2106b 100644
--- a/contrib/romega/g_romega.ml4
+++ b/contrib/romega/g_romega.ml4
@@ -9,7 +9,34 @@
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
 open Refl_omega
+open Refiner
 
-TACTIC EXTEND romelga
-  [ "romega" ] -> [ total_reflexive_omega_tactic ]
+let romega_tactic l = 
+  let tacs = List.map 
+    (function  
+       | "nat" -> Tacinterp.interp <:tactic<zify_nat>>
+       | "positive" -> Tacinterp.interp <:tactic<zify_positive>>
+       | "N" -> Tacinterp.interp <:tactic<zify_N>>
+       | "Z" -> Tacinterp.interp <:tactic<zify_op>>
+       | s -> Util.error ("No ROmega knowledge base for type "^s))
+    (Util.list_uniquize (List.sort compare l))
+  in 
+  tclTHEN
+    (tclREPEAT (tclPROGRESS (tclTHENLIST tacs)))
+    (tclTHEN 
+       (* because of the contradiction process in (r)omega, 
+          we'd better leave as little as possible in the conclusion,
+          for an easier decidability argument. *)
+       Tactics.intros 
+       total_reflexive_omega_tactic)
+
+
+TACTIC EXTEND romega
+|  [ "romega" ] -> [ romega_tactic [] ]
+END
+
+TACTIC EXTEND romega'
+| [ "romega" "with" ne_ident_list(l) ] -> 
+    [ romega_tactic (List.map Names.string_of_id l) ]
+| [ "romega" "with" "*" ] -> [ romega_tactic ["nat";"positive";"N";"Z"] ]
 END
diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v
index 2d29a8356b..ecbf04e412 100644
--- a/test-suite/success/Omega.v
+++ b/test-suite/success/Omega.v
@@ -10,14 +10,14 @@ intros x y.
  omega.
 Qed.
 
-(* Proposed by Pierre Crégut *)
+(* Proposed by Pierre Crégut *)
 
 Lemma lem2 : forall x : Z, (x < 4)%Z -> (x > 2)%Z -> x = 3%Z.
 intro.
  omega.
 Qed.
 
-(* Proposed by Jean-Christophe Filliâtre *)
+(* Proposed by Jean-Christophe Filliâtre *)
 
 Lemma lem3 : forall x y : Z, x = y -> (x + x)%Z = (y + y)%Z.
 Proof.
@@ -25,7 +25,7 @@ intros.
  omega.
 Qed.
 
-(* Proposed by Jean-Christophe Filliâtre: confusion between an Omega *)
+(* Proposed by Jean-Christophe Filliâtre: confusion between an Omega *)
 (* internal variable and a section variable (June 2001) *)
 
 Section A.
@@ -87,10 +87,8 @@ Qed.
 
 (* Check that the interpretation of mult on nat enforces its positivity *)
 (* Submitted by Hubert Thierry (bug #743) *)
-(* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z"
-Require Omega.
-Lemma lem10 : (n, m : nat) (le n (plus n (mult n m))).
+(* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z" *)
+Lemma lem10 : forall n m:nat, le n (plus n (mult n m)).
 Proof.
-Intros; Omega.
+intros; omega with *.
 Qed.
-*)
diff --git a/test-suite/success/OmegaPre.v b/test-suite/success/OmegaPre.v
new file mode 100644
index 0000000000..bb800b7a01
--- /dev/null
+++ b/test-suite/success/OmegaPre.v
@@ -0,0 +1,127 @@
+Require Import ZArith Nnat Omega.
+Open Scope Z_scope.
+
+(** Test of the zify preprocessor for (R)Omega *)
+
+(* More details in file PreOmega.v
+ 
+   (r)omega with Z        : starts with zify_op
+   (r)omega with nat      : starts with zify_nat
+   (r)omega with positive : starts with zify_positive
+   (r)omega with N        : starts with uses zify_N
+   (r)omega with *        : starts zify (a saturation of the others)
+*)
+
+(* zify_op *)
+
+Goal forall a:Z, Zmax a a = a.
+intros.
+omega with *.
+Qed.
+
+Goal forall a b:Z, Zmax a b = Zmax b a.
+intros.
+omega with *.
+Qed.
+
+Goal forall a b c:Z, Zmax a (Zmax b c) = Zmax (Zmax a b) c.
+intros.
+omega with *.
+Qed.
+
+Goal forall a b:Z, Zmax a b + Zmin a b = a + b.
+intros.
+omega with *.
+Qed.
+
+Goal forall a:Z, (Zabs a)*(Zsgn a) = a.
+intros.
+zify.
+intuition; subst; omega. (* pure multiplication: omega alone can't do it *)
+Qed.
+
+Goal forall a:Z, Zabs a = a -> a >= 0.
+intros.
+omega with *.
+Qed.
+
+Goal forall a:Z, Zsgn a = a -> a = 1 \/ a = 0 \/ a = -1.
+intros.
+omega with *.
+Qed.
+
+(* zify_nat *)
+
+Goal forall m: nat, (m<2)%nat -> (0<= m+m <=2)%nat.
+intros.
+omega with *.
+Qed.
+
+Goal forall m:nat, (m<1)%nat -> (m=0)%nat.
+intros.
+omega with *.
+Qed.
+
+Goal forall m: nat, (m<=100)%nat -> (0<= m+m <=200)%nat.
+intros.
+omega with *.
+Qed.
+(* 2000 instead of 200: works, but quite slow *)
+
+Goal forall m: nat, (m*m>=0)%nat.
+intros.
+omega with *.
+Qed.
+
+(* zify_positive *)
+
+Goal forall m: positive, (m<2)%positive -> (2 <= m+m /\ m+m <= 2)%positive.
+intros.
+omega with *.
+Qed.
+
+Goal forall m:positive, (m<2)%positive -> (m=1)%positive.
+intros.
+omega with *.
+Qed.
+
+Goal forall m: positive, (m<=1000)%positive -> (2<=m+m/\m+m <=2000)%positive.
+intros.
+omega with *.
+Qed.
+
+Goal forall m: positive, (m*m>=1)%positive.
+intros.
+omega with *.
+Qed.
+
+(* zify_N *)
+
+Goal forall m:N, (m<2)%N -> (0 <= m+m /\ m+m <= 2)%N.
+intros.
+omega with *.
+Qed.
+
+Goal forall m:N, (m<1)%N -> (m=0)%N.
+intros.
+omega with *.
+Qed.
+
+Goal forall m:N, (m<=1000)%N -> (0<=m+m/\m+m <=2000)%N.
+intros.
+omega with *.
+Qed.
+
+Goal forall m:N, (m*m>=0)%N.
+intros.
+omega with *.
+Qed.
+
+(* mix of datatypes *)
+
+Goal forall p, Z_of_N (N_of_nat (nat_of_N (Npos p))) = Zpos p.
+intros.
+omega with *.
+Qed.
+
+
diff --git a/test-suite/success/ROmega.v b/test-suite/success/ROmega.v
index ff1f57df32..0c37c59aca 100644
--- a/test-suite/success/ROmega.v
+++ b/test-suite/success/ROmega.v
@@ -68,31 +68,29 @@ Variable n : nat.
 Variable ap_n : n <> 0.
 Let delta := f n ap_n.
 Lemma lem7 : n = n.
- (*romega. ---> ROMEGA CANT DEAL WITH NAT*)
-Admitted.
+ romega with nat.
+Qed.
 End C.
 
 (* Problem of dependencies *)
 Require Import Omega.
 Lemma lem8 : forall H : 0 = 0 -> 0 = 0, H = H -> 0 = 0.
 intros.
-(* romega. ---> ROMEGA CANT DEAL WITH NAT*)
-Admitted.
+romega with nat.
+Qed.
 
 (* Bug that what caused by the use of intro_using in Omega *)
 Require Import Omega.
 Lemma lem9 :
  forall p q : nat, ~ (p <= q /\ p < q \/ q <= p /\ p < q) -> p < p \/ p <= p.
 intros.
-(* romega. ---> ROMEGA CANT DEAL WITH NAT*) 
-Admitted.
+romega with nat.
+Qed.
 
 (* Check that the interpretation of mult on nat enforces its positivity *)
 (* Submitted by Hubert Thierry (bug #743) *)
-(* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z"
-Require Omega.
-Lemma lem10 : (n, m : nat) (le n (plus n (mult n m))).
+(* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z" *)
+Lemma lem10 : forall n m : nat, le n (plus n (mult n m)).
 Proof.
-Intros; Omega.
+intros; romega with nat.
 Qed.
-*)
diff --git a/test-suite/success/ROmegaPre.v b/test-suite/success/ROmegaPre.v
new file mode 100644
index 0000000000..550edca507
--- /dev/null
+++ b/test-suite/success/ROmegaPre.v
@@ -0,0 +1,127 @@
+Require Import ZArith Nnat ROmega.
+Open Scope Z_scope.
+
+(** Test of the zify preprocessor for (R)Omega *)
+
+(* More details in file PreOmega.v
+ 
+   (r)omega with Z        : starts with zify_op
+   (r)omega with nat      : starts with zify_nat
+   (r)omega with positive : starts with zify_positive
+   (r)omega with N        : starts with uses zify_N
+   (r)omega with *        : starts zify (a saturation of the others)
+*)
+
+(* zify_op *)
+
+Goal forall a:Z, Zmax a a = a.
+intros.
+romega with *.
+Qed.
+
+Goal forall a b:Z, Zmax a b = Zmax b a.
+intros.
+romega with *.
+Qed.
+
+Goal forall a b c:Z, Zmax a (Zmax b c) = Zmax (Zmax a b) c.
+intros.
+romega with *.
+Qed.
+
+Goal forall a b:Z, Zmax a b + Zmin a b = a + b.
+intros.
+romega with *.
+Qed.
+
+Goal forall a:Z, (Zabs a)*(Zsgn a) = a.
+intros.
+zify.
+intuition; subst; romega. (* pure multiplication: omega alone can't do it *)
+Qed.
+
+Goal forall a:Z, Zabs a = a -> a >= 0.
+intros.
+romega with *.
+Qed.
+
+Goal forall a:Z, Zsgn a = a -> a = 1 \/ a = 0 \/ a = -1.
+intros.
+romega with *.
+Qed.
+
+(* zify_nat *)
+
+Goal forall m: nat, (m<2)%nat -> (0<= m+m <=2)%nat.
+intros.
+romega with *.
+Qed.
+
+Goal forall m:nat, (m<1)%nat -> (m=0)%nat.
+intros.
+romega with *.
+Qed.
+
+Goal forall m: nat, (m<=100)%nat -> (0<= m+m <=200)%nat.
+intros.
+romega with *.
+Qed.
+(* 2000 instead of 200: works, but quite slow *)
+
+Goal forall m: nat, (m*m>=0)%nat.
+intros.
+romega with *.
+Qed.
+
+(* zify_positive *)
+
+Goal forall m: positive, (m<2)%positive -> (2 <= m+m /\ m+m <= 2)%positive.
+intros.
+romega with *.
+Qed.
+
+Goal forall m:positive, (m<2)%positive -> (m=1)%positive.
+intros.
+romega with *.
+Qed.
+
+Goal forall m: positive, (m<=1000)%positive -> (2<=m+m/\m+m <=2000)%positive.
+intros.
+romega with *.
+Qed.
+
+Goal forall m: positive, (m*m>=1)%positive.
+intros.
+romega with *.
+Qed.
+
+(* zify_N *)
+
+Goal forall m:N, (m<2)%N -> (0 <= m+m /\ m+m <= 2)%N.
+intros.
+romega with *.
+Qed.
+
+Goal forall m:N, (m<1)%N -> (m=0)%N.
+intros.
+romega with *.
+Qed.
+
+Goal forall m:N, (m<=1000)%N -> (0<=m+m/\m+m <=2000)%N.
+intros.
+romega with *.
+Qed.
+
+Goal forall m:N, (m*m>=0)%N.
+intros.
+romega with *.
+Qed.
+
+(* mix of datatypes *)
+
+Goal forall p, Z_of_N (N_of_nat (nat_of_N (Npos p))) = Zpos p.
+intros.
+romega with *.
+Qed.
+
+
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index cc2d04e58c..6e4c4b26f0 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -416,7 +416,7 @@ Ltac bal_tac :=
 
 Ltac bal_tac_imp := match goal with 
   | |- context [ assert_false ] => 
-      inv avl; avl_nns; simpl in *; false_omega
+      inv avl; avl_nns; simpl in *; omega_max
   | _ => idtac
 end.
 
@@ -703,7 +703,7 @@ Proof.
  rewrite e3; simpl;destruct 1.
  split.
  apply bal_avl; auto.
- simpl; omega_max.
+ omega_max.
  omega_bal.
 Qed.
 
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index 23d42fda8b..fa10809cc7 100644
--- a/theories/FSets/FSetAVL.v
+++ b/theories/FSets/FSetAVL.v
@@ -461,7 +461,7 @@ Lemma bal_in : forall l x r y, avl l -> avl r ->
 Proof.
  bal_tac; 
  solve [repeat rewrite create_in; intuition_in
-       |inv avl; avl_nns; simpl in *; false_omega].
+       |inv avl; avl_nns; simpl in *; omega_max].
 Qed.
 
 Ltac omega_bal := match goal with 
@@ -1856,7 +1856,7 @@ Qed.
 Lemma height_0 : forall s, avl s -> height s = 0 -> s = Leaf.
 Proof.
  destruct 1; intuition; simpl in *.
- avl_nns; simpl in *; false_omega_max.
+ avl_nns; simpl in *; elimtype False; omega_max.
 Qed.   
 
 (** * Union
diff --git a/theories/Ints/Z/IntsZmisc.v b/theories/Ints/Z/IntsZmisc.v
index 6fcaaa6e9f..e4dee2d4f6 100644
--- a/theories/Ints/Z/IntsZmisc.v
+++ b/theories/Ints/Z/IntsZmisc.v
@@ -100,7 +100,7 @@ Definition is_lt (n m : positive) :=
   end.
 Infix "?<" := is_lt (at level 70, no associativity) : P_scope.
 
-Lemma is_lt_spec : forall n m, if n ?< m then n < m else m <= n. 
+Lemma is_lt_spec : forall n m, if n ?< m then (n < m)%Z else (m <= n)%Z. 
 Proof.
  intros n m; unfold is_lt, Zlt, Zle, Zcompare.
  rewrite (ZC4 m n);destruct ((n ?= m) Eq);trivial;try (intro;discriminate).
diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v
index 2e3c6a3a5b..28c6fdb6d6 100644
--- a/theories/NArith/BinPos.v
+++ b/theories/NArith/BinPos.v
@@ -220,6 +220,22 @@ Fixpoint Pcompare (x y:positive) (r:comparison) {struct y} : comparison :=
 
 Infix "?=" := Pcompare (at level 70, no associativity) : positive_scope.
 
+Definition Plt (x y:positive) := (Pcompare x y Eq) = Lt.
+Definition Pgt (x y:positive) := (Pcompare x y Eq) = Gt.
+Definition Ple (x y:positive) := (Pcompare x y Eq) <> Gt.
+Definition Pge (x y:positive) := (Pcompare x y Eq) <> Lt.
+
+Infix "<=" := Ple : positive_scope.
+Infix "<" := Plt : positive_scope.
+Infix ">=" := Pge : positive_scope.
+Infix ">" := Pgt : positive_scope.
+
+Notation "x <= y <= z" := (x <= y /\ y <= z) : positive_scope.
+Notation "x <= y < z" := (x <= y /\ y < z) : positive_scope.
+Notation "x < y < z" := (x < y /\ y < z) : positive_scope.
+Notation "x < y <= z" := (x < y /\ y <= z) : positive_scope.
+
+
 Definition Pmin (p p' : positive) := match Pcompare p p' Eq with 
  | Lt | Eq => p 
  | Gt => p'
@@ -959,6 +975,11 @@ Qed.
 (**********************************************************************)
 (** Properties of subtraction on binary positive numbers *)
 
+Lemma Ppred_minus : forall p, Ppred p = Pminus p xH.
+Proof.
+  destruct p; compute; auto.
+Qed.
+
 Lemma double_eq_zero_inversion :
   forall p:positive_mask, Pdouble_mask p = IsNul -> p = IsNul.
 Proof.
@@ -991,6 +1012,33 @@ Proof.
       | auto ].
 Qed.
 
+Lemma Pminus_mask_carry_diag : forall p, Pminus_mask_carry p p = IsNeg.
+Proof.
+  induction p; simpl; auto; rewrite IHp; auto.
+Qed.
+
+Lemma Pminus_mask_IsNeg : forall p q:positive, 
+ Pminus_mask p q = IsNeg -> Pminus_mask_carry p q = IsNeg.
+Proof.
+  induction p; destruct q; simpl; intros; auto; try discriminate.
+
+  unfold Pdouble_mask in H.
+  generalize (IHp q).
+  destruct (Pminus_mask p q); try discriminate.
+  intro H'; rewrite H'; auto.
+
+  unfold Pdouble_plus_one_mask in H.
+  destruct (Pminus_mask p q); simpl; auto; try discriminate.
+
+  unfold Pdouble_plus_one_mask in H.
+  destruct (Pminus_mask_carry p q); simpl; auto; try discriminate.
+
+  unfold Pdouble_mask in H.
+  generalize (IHp q).
+  destruct (Pminus_mask p q); try discriminate.
+  intro H'; rewrite H'; auto.
+Qed.
+
 Lemma ZL10 :
   forall p q:positive,
     Pminus_mask p q = IsPos xH -> Pminus_mask_carry p q = IsNul.
@@ -1099,3 +1147,26 @@ Proof.
     intros H2 H3; elim H3; intros H4 H5; unfold Pminus in |- *; 
       rewrite H2; exact H4.
 Qed.
+
+(* When x<y, the substraction of x by y returns 1 *)
+
+Lemma Pminus_mask_Lt : forall p q:positive, p<q -> Pminus_mask p q = IsNeg.
+Proof.
+  unfold Plt; induction p; destruct q; simpl; intros; auto; try discriminate.
+  rewrite IHp; simpl; auto.
+  rewrite IHp; simpl; auto.
+  apply Pcompare_Gt_Lt; auto.
+  destruct (Pcompare_Lt_Lt _ _ H).
+  rewrite Pminus_mask_IsNeg; simpl; auto.
+  subst q; rewrite Pminus_mask_carry_diag; auto.
+  rewrite IHp; simpl; auto.
+Qed. 
+
+Lemma Pminus_Lt : forall p q:positive, p<q -> p-q = xH.
+Proof.
+  intros; unfold Plt, Pminus; rewrite Pminus_mask_Lt; auto.
+Qed.
+
+
+
+
diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v
index e19989aed9..76a3d616c9 100644
--- a/theories/NArith/Nnat.v
+++ b/theories/NArith/Nnat.v
@@ -16,7 +16,11 @@ Require Import Min.
 Require Import Max.
 Require Import BinPos.
 Require Import BinNat.
+Require Import BinInt.
 Require Import Pnat.
+Require Import Zmax.
+Require Import Zmin.
+Require Import Znat.
 
 (** Translation from [N] to [nat] and back. *)
 
@@ -238,3 +242,136 @@ Proof.
   rewrite <- nat_of_Nmax.
   apply N_of_nat_of_N.
 Qed.
+
+(** Properties concerning Z_of_N *)
+
+Lemma Z_of_nat_of_N : forall n:N, Z_of_nat (nat_of_N n) = Z_of_N n.
+Proof.
+  destruct n; simpl; auto; symmetry; apply Zpos_eq_Z_of_nat_o_nat_of_P.
+Qed.
+
+Lemma Z_of_N_eq : forall n m, n = m -> Z_of_N n = Z_of_N m.
+Proof.
+ intros; f_equal; assumption.
+Qed.
+
+Lemma Z_of_N_eq_rev : forall n m, Z_of_N n = Z_of_N m -> n = m.
+Proof.
+ intros [|n] [|m]; simpl; intros; try discriminate; congruence.
+Qed.
+
+Lemma Z_of_N_eq_iff : forall n m, n = m <-> Z_of_N n = Z_of_N m.
+Proof.
+ split; [apply Z_of_N_eq | apply Z_of_N_eq_rev].
+Qed.
+
+Lemma Z_of_N_le : forall n m, (n<=m)%N -> (Z_of_N n <= Z_of_N m)%Z.
+Proof.
+ intros [|n] [|m]; simpl; auto.
+Qed.
+
+Lemma Z_of_N_le_rev : forall n m, (Z_of_N n <= Z_of_N m)%Z -> (n<=m)%N.
+Proof.
+ intros [|n] [|m]; simpl; auto.
+Qed.
+
+Lemma Z_of_N_le_iff : forall n m, (n<=m)%N <-> (Z_of_N n <= Z_of_N m)%Z.
+Proof.
+ split; [apply Z_of_N_le | apply Z_of_N_le_rev].
+Qed.
+
+Lemma Z_of_N_lt : forall n m, (n<m)%N -> (Z_of_N n < Z_of_N m)%Z.
+Proof.
+ intros [|n] [|m]; simpl; auto.
+Qed.
+
+Lemma Z_of_N_lt_rev : forall n m, (Z_of_N n < Z_of_N m)%Z -> (n<m)%N.
+Proof.
+ intros [|n] [|m]; simpl; auto.
+Qed.
+
+Lemma Z_of_N_lt_iff : forall n m, (n<m)%N <-> (Z_of_N n < Z_of_N m)%Z.
+Proof.
+ split; [apply Z_of_N_lt | apply Z_of_N_lt_rev].
+Qed.
+
+Lemma Z_of_N_ge : forall n m, (n>=m)%N -> (Z_of_N n >= Z_of_N m)%Z.
+Proof.
+ intros [|n] [|m]; simpl; auto.
+Qed.
+
+Lemma Z_of_N_ge_rev : forall n m, (Z_of_N n >= Z_of_N m)%Z -> (n>=m)%N.
+Proof.
+ intros [|n] [|m]; simpl; auto.
+Qed.
+
+Lemma Z_of_N_ge_iff : forall n m, (n>=m)%N <-> (Z_of_N n >= Z_of_N m)%Z.
+Proof.
+ split; [apply Z_of_N_ge | apply Z_of_N_ge_rev].
+Qed.
+
+Lemma Z_of_N_gt : forall n m, (n>m)%N -> (Z_of_N n > Z_of_N m)%Z.
+Proof.
+ intros [|n] [|m]; simpl; auto.
+Qed.
+
+Lemma Z_of_N_gt_rev : forall n m, (Z_of_N n > Z_of_N m)%Z -> (n>m)%N.
+Proof.
+ intros [|n] [|m]; simpl; auto.
+Qed.
+
+Lemma Z_of_N_gt_iff : forall n m, (n>m)%N <-> (Z_of_N n > Z_of_N m)%Z.
+Proof.
+ split; [apply Z_of_N_gt | apply Z_of_N_gt_rev].
+Qed.
+
+Lemma Z_of_N_of_nat : forall n:nat, Z_of_N (N_of_nat n) = Z_of_nat n.
+Proof.
+ destruct n; simpl; auto.
+Qed. 
+
+Lemma Z_of_N_pos : forall p:positive, Z_of_N (Npos p) = Zpos p.
+Proof.
+ destruct p; simpl; auto.
+Qed. 
+
+Lemma Z_of_N_abs : forall z:Z, Z_of_N (Zabs_N z) = Zabs z.
+Proof.
+ destruct z; simpl; auto.
+Qed. 
+
+Lemma Z_of_N_le_0 : forall n, (0 <= Z_of_N n)%Z.
+Proof.
+ destruct n; intro; discriminate.
+Qed.
+
+Lemma Z_of_N_plus : forall n m:N, Z_of_N (n+m) = (Z_of_N n + Z_of_N m)%Z.
+Proof.
+intros; repeat rewrite <- Z_of_nat_of_N; rewrite nat_of_Nplus; apply inj_plus.
+Qed.
+
+Lemma Z_of_N_mult : forall n m:N, Z_of_N (n*m) = (Z_of_N n * Z_of_N m)%Z.
+Proof.
+intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nmult; apply inj_mult.
+Qed.
+
+Lemma Z_of_N_minus : forall n m:N, Z_of_N (n-m) = Zmax 0 (Z_of_N n - Z_of_N m). 
+Proof.
+intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nminus; apply inj_minus.
+Qed.
+
+Lemma Z_of_N_succ : forall n:N, Z_of_N (Nsucc n) = Zsucc (Z_of_N n). 
+Proof.
+intros; do 2 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nsucc; apply inj_S.
+Qed.
+
+Lemma Z_of_N_min : forall n m:N, Z_of_N (Nmin n m) = Zmin (Z_of_N n) (Z_of_N m). 
+Proof.
+intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nmin; apply inj_min.
+Qed.
+
+Lemma Z_of_N_max : forall n m:N, Z_of_N (Nmax n m) = Zmax (Z_of_N n) (Z_of_N m). 
+Proof.
+intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nmax; apply inj_max.
+Qed.
+
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index d5cd17a0c4..5bc81f955f 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -9,7 +9,7 @@
 (*i $Id$ i*)
 
 (***********************************************************)
-(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
+(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
 (***********************************************************)
 
 Require Export BinPos.
@@ -967,6 +967,21 @@ Qed.
 (**********************************************************************)
 (** * Relating binary positive numbers and binary integers *)
 
+Lemma Zpos_eq : forall p q, p = q -> Zpos p = Zpos q.
+Proof.
+  intros; f_equal; auto.
+Qed.
+
+Lemma Zpos_eq_rev : forall p q, Zpos p = Zpos q -> p = q.
+Proof.
+  inversion 1; auto.
+Qed.
+
+Lemma Zpos_eq_iff : forall p q, p = q <-> Zpos p = Zpos q.
+Proof.
+  split; [apply Zpos_eq|apply Zpos_eq_rev].
+Qed.
+
 Lemma Zpos_xI : forall p:positive, Zpos (xI p) = Zpos 2 * Zpos p + Zpos 1.
 Proof.
   intro; apply refl_equal.
@@ -1061,3 +1076,4 @@ Definition Z_of_N (x:N) := match x with
                              | N0 => Z0
                              | Npos p => Zpos p
                            end.
+
diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v
index 4c9470b36e..562000d8fd 100644
--- a/theories/ZArith/Int.v
+++ b/theories/ZArith/Int.v
@@ -7,8 +7,8 @@
 (***********************************************************************)
 
 (* Finite sets library.  
- * Authors: Pierre Letouzey and Jean-Christophe Filliâtre 
- * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
+ * Authors: Pierre Letouzey and Jean-Christophe Filliâtre 
+ * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
  *              91405 Orsay, France *)
 
 (* $Id$ *)
@@ -352,46 +352,15 @@ Module MoreInt (I:Int).
   Ltac i2z_refl := 
     i2z_gen;
     match goal with |- ?t => 
-      let e := p2ep t 
-	in 
-	(change (ep2p e); 
-	  apply norm_ep_correct2; 
-	    simpl)
+      let e := p2ep t in 
+      change (ep2p e); apply norm_ep_correct2; simpl
     end.
 
-  Ltac iauto := i2z_refl; auto.
-  Ltac iomega := i2z_refl; intros; romega.
-
-  Open Scope Z_scope.
-
-  Lemma max_spec : forall (x y:Z), 
-    x >= y /\ Zmax x y = x  \/
-    x < y /\ Zmax x y = y.
-  Proof.
-    intros; unfold Zmax, Zlt, Zge.
-    destruct (Zcompare x y); [ left | right | left ]; split; auto; discriminate.
-  Qed.
-
-  Ltac omega_max_genspec x y := 
-    generalize (max_spec x y); 
-    (let z := fresh "z" in let Hz := fresh "Hz" in 
-     set (z:=Zmax x y); clearbody z).
-
-  Ltac omega_max_loop := 
-    match goal with 
-      (* hack: we don't want [i2z (height ...)] to be reduced by romega later... *)
-      | |- context [ i2z (?f ?x) ] => 
-          let i := fresh "i2z" in (set (i:=i2z (f x)); clearbody i); omega_max_loop
-      | |- context [ Zmax ?x ?y ] => omega_max_genspec x y; omega_max_loop
-      | _ => intros
-    end.
-
-  Ltac omega_max := i2z_refl; omega_max_loop; try romega.
+  (* i2z_refl can be replaced below by (simpl in *; i2z). 
+     The reflexive version improves compilation of AVL files by about 15%  *)
   
-  Ltac false_omega := i2z_refl; intros; romega.
-  Ltac false_omega_max := elimtype False; omega_max.
+  Ltac omega_max := i2z_refl; romega with Z.
 
-  Open Scope Int_scope.
 End MoreInt.
 
 
diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v
index c7f0bb7232..e43d68bfa1 100644
--- a/theories/ZArith/Zabs.v
+++ b/theories/ZArith/Zabs.v
@@ -7,7 +7,7 @@
 (************************************************************************)
 (*i $Id$ i*)
 
-(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
+(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
 
 Require Import Arith_base.
 Require Import BinPos.
@@ -70,6 +70,13 @@ Proof.
       (intros H2; rewrite H2); auto.
 Qed.
 
+Lemma Zabs_spec : forall x:Z, 
+  0 <= x /\ Zabs x = x \/ 
+  0 > x /\ Zabs x = -x. 
+Proof.
+ intros; unfold Zabs, Zle, Zgt; destruct x; simpl; intuition discriminate.
+Qed.
+
 (** * Triangular inequality *)
 
 Hint Local Resolve Zle_neg_pos: zarith.
@@ -89,6 +96,16 @@ Proof.
   apply Zplus_le_compat; simpl in |- *; auto with zarith.
 Qed.
 
+(** * A characterization of the sign function: *)
+
+Lemma Zsgn_spec : forall x:Z, 
+  0 < x /\ Zsgn x = 1 \/ 
+  0 = x /\ Zsgn x = 0 \/ 
+  0 > x /\ Zsgn x = -1.
+Proof. 
+ intros; unfold Zsgn, Zle, Zgt; destruct x; compute; intuition.
+Qed.
+
 (** * Absolute value and multiplication *)
 
 Lemma Zsgn_Zabs : forall n:Z, n * Zsgn n = Zabs n.
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index b7121fa197..33f50fc9b7 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -10,7 +10,7 @@
 
 Require Import ZArithRing.
 Require Import ZArith_base.
-Require Import Omega.
+Require Export Omega.
 Require Import Wf_nat.
 Open Local Scope Z_scope.
 
diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v
index b2c0685640..fbc7bfafc7 100644
--- a/theories/ZArith/Zmax.v
+++ b/theories/ZArith/Zmax.v
@@ -38,6 +38,14 @@ Proof.
   destruct (n ?= m); (apply H1|| apply H2); discriminate. 
 Qed.
 
+Lemma Zmax_spec : forall x y:Z, 
+  x >= y /\ Zmax x y = x  \/
+  x < y /\ Zmax x y = y.
+Proof.
+ intros; unfold Zmax, Zlt, Zge.
+ destruct (Zcompare x y); [ left | right | left ]; split; auto; discriminate.
+Qed.
+
 (** * Least upper bound properties of max *)
 
 Lemma Zle_max_l : forall n m:Z, n <= Zmax n m.
@@ -106,3 +114,39 @@ Proof.
     rewrite (Zcompare_plus_compat x y n).
   case (x ?= y); apply Zplus_comm.
 Qed.
+
+(** * Maximum and Zpos *)
+
+Lemma Zpos_max : forall p q, Zpos (Pmax p q) = Zmax (Zpos p) (Zpos q).
+Proof.
+  intros; unfold Zmax, Pmax; simpl; generalize (Pcompare_Eq_eq p q).
+  destruct Pcompare; auto.
+  intro H; rewrite H; auto.
+Qed.
+
+Lemma Zpos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p.
+Proof.
+  intros; unfold Zmax; simpl; destruct p; simpl; auto.
+Qed.
+
+(** * Characterization of Pminus in term of Zminus and Zmax *)
+
+Lemma Zpos_minus : forall p q, Zpos (Pminus p q) = Zmax 1 (Zpos p - Zpos q).
+Proof.
+  intros.
+  case_eq (Pcompare p q Eq).
+  intros H; rewrite (Pcompare_Eq_eq _ _ H).
+  rewrite Zminus_diag.
+  unfold Zmax; simpl.
+  unfold Pminus; rewrite Pminus_mask_diag; auto.
+  intros; rewrite Pminus_Lt; auto.
+  destruct (Zmax_spec 1 (Zpos p - Zpos q)) as [(H1,H2)|(H1,H2)]; auto.
+  elimtype False; clear H2.
+  assert (H1':=Zlt_trans 0 1 _ Zlt_0_1 H1).
+  generalize (Zlt_0_minus_lt _ _ H1').
+  unfold Zlt; simpl.
+  rewrite (ZC2 _ _ H); intro; discriminate.
+  intros; simpl; rewrite H.
+  symmetry; apply Zpos_max_1.
+Qed.
+
diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v
index 0e0caa1bd6..beb91a738b 100644
--- a/theories/ZArith/Zmin.v
+++ b/theories/ZArith/Zmin.v
@@ -7,7 +7,7 @@
 (************************************************************************)
 (*i $Id$ i*)
 
-(** Initial version from Pierre Crégut (CNET, Lannion, France), 1996.
+(** Initial version from Pierre Crégut (CNET, Lannion, France), 1996.
     Further extensions by the Coq development team, with suggestions
     from Russell O'Connor (Radbout U., Nijmegen, The Netherlands).
  *)
@@ -43,6 +43,14 @@ Proof.
   intros n m P H1 H2; unfold Zmin in |- *; case (n ?= m); auto with arith.
 Qed.
 
+Lemma Zmin_spec : forall x y:Z, 
+  x <= y /\ Zmin x y = x  \/
+  x > y /\ Zmin x y = y.
+Proof.
+ intros; unfold Zmin, Zle, Zgt.
+ destruct (Zcompare x y); [ left | left | right ]; split; auto; discriminate.
+Qed.
+
 (** * Greatest lower bound properties of min *)
 
 Lemma Zle_min_l : forall n m:Z, Zmin n m <= n.
@@ -128,3 +136,11 @@ Proof.
 Qed.
 
 Notation Zmin_plus := Zplus_min_distr_r (only parsing).
+
+(** * Minimum and Zpos *)
+
+Lemma Zpos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q).
+Proof.
+  intros; unfold Zmin, Pmin; simpl; destruct Pcompare; auto.
+Qed.
+
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index 27f31bf83b..d9fb4e97c2 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
+(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
 
 Require Export Arith_base.
 Require Import BinPos.
@@ -17,6 +17,7 @@ Require Import Zcompare.
 Require Import Zorder.
 Require Import Decidable.
 Require Import Peano_dec.
+Require Import Min Max Zmin Zmax.
 Require Export Compare_dec.
 
 Open Local Scope Z_scope.
@@ -26,6 +27,8 @@ Definition neq (x y:nat) := x <> y.
 (************************************************)
 (** Properties of the injection from nat into Z *)
 
+(** Injection and successor *)
+
 Theorem inj_S : forall n:nat, Z_of_nat (S n) = Zsucc (Z_of_nat n).
 Proof.
   intro y; induction y as [| n H];
@@ -33,25 +36,12 @@ Proof.
       | change (Zpos (Psucc (P_of_succ_nat n)) = Zsucc (Z_of_nat (S n))) in |- *;
 	rewrite Zpos_succ_morphism; trivial with arith ].
 Qed.
- 
-Theorem inj_plus : forall n m:nat, Z_of_nat (n + m) = Z_of_nat n + Z_of_nat m.
-Proof.
-  intro x; induction x as [| n H]; intro y; destruct y as [| m];
-    [ simpl in |- *; trivial with arith
-      | simpl in |- *; trivial with arith
-      | simpl in |- *; rewrite <- plus_n_O; trivial with arith
-      | change (Z_of_nat (S (n + S m)) = Z_of_nat (S n) + Z_of_nat (S m)) in |- *;
-	rewrite inj_S; rewrite H; do 2 rewrite inj_S; rewrite Zplus_succ_l;
-	  trivial with arith ].
-Qed.
 
-Theorem inj_mult : forall n m:nat, Z_of_nat (n * m) = Z_of_nat n * Z_of_nat m.
+(** Injection and equality. *)
+
+Theorem inj_eq : forall n m:nat, n = m -> Z_of_nat n = Z_of_nat m.
 Proof.
-  intro x; induction x as [| n H];
-    [ simpl in |- *; trivial with arith
-      | intro y; rewrite inj_S; rewrite <- Zmult_succ_l_reverse; rewrite <- H;
-	rewrite <- inj_plus; simpl in |- *; rewrite plus_comm; 
-	  trivial with arith ].
+  intros x y H; rewrite H; trivial with arith.
 Qed.
 
 Theorem inj_neq : forall n m:nat, neq n m -> Zne (Z_of_nat n) (Z_of_nat m).
@@ -66,6 +56,24 @@ Proof.
 	    intros E; rewrite E; auto with arith ].
 Qed. 
 
+Theorem inj_eq_rev : forall n m:nat, Z_of_nat n = Z_of_nat m -> n = m.
+Proof.
+  intros x y H.
+  destruct (eq_nat_dec x y) as [H'|H']; auto.
+  elimtype False.
+  exact (inj_neq _ _ H' H).
+Qed.
+
+Theorem inj_eq_iff : forall n m:nat, n=m <-> Z_of_nat n = Z_of_nat m.
+Proof.
+ split; [apply inj_eq | apply inj_eq_rev].
+Qed.
+
+
+(** Injection and order relations: *)
+
+(** One way ... *)
+
 Theorem inj_le : forall n m:nat, (n <= m)%nat -> Z_of_nat n <= Z_of_nat m.
 Proof.
   intros x y; intros H; elim H;
@@ -81,29 +89,100 @@ Proof.
     exact H.
 Qed.
 
+Theorem inj_ge : forall n m:nat, (n >= m)%nat -> Z_of_nat n >= Z_of_nat m.
+Proof.
+  intros x y H; apply Zle_ge; apply inj_le; apply H.
+Qed.
+
 Theorem inj_gt : forall n m:nat, (n > m)%nat -> Z_of_nat n > Z_of_nat m.
 Proof.
   intros x y H; apply Zlt_gt; apply inj_lt; exact H.
 Qed.
 
-Theorem inj_ge : forall n m:nat, (n >= m)%nat -> Z_of_nat n >= Z_of_nat m.
+(** The other way ... *)
+
+Theorem inj_le_rev : forall n m:nat, Z_of_nat n <= Z_of_nat m -> (n <= m)%nat.
 Proof.
-  intros x y H; apply Zle_ge; apply inj_le; apply H.
+  intros x y H.
+  destruct (le_lt_dec x y) as [H0|H0]; auto.
+  elimtype False.
+  assert (H1:=inj_lt _ _ H0).
+  red in H; red in H1.
+  rewrite <- Zcompare_antisym in H; rewrite H1 in H; auto.
 Qed.
 
-Theorem inj_eq : forall n m:nat, n = m -> Z_of_nat n = Z_of_nat m.
+Theorem inj_lt_rev : forall n m:nat, Z_of_nat n < Z_of_nat m -> (n < m)%nat.
 Proof.
-  intros x y H; rewrite H; trivial with arith.
+  intros x y H.
+  destruct (le_lt_dec y x) as [H0|H0]; auto.
+  elimtype False.
+  assert (H1:=inj_le _ _ H0).
+  red in H; red in H1.
+  rewrite <- Zcompare_antisym in H1; rewrite H in H1; auto.
 Qed.
 
-Theorem intro_Z :
-  forall n:nat,  exists y : Z, Z_of_nat n = y /\ 0 <= y * 1 + 0.
+Theorem inj_ge_rev : forall n m:nat, Z_of_nat n >= Z_of_nat m -> (n >= m)%nat.
 Proof.
-  intros x; exists (Z_of_nat x); split;
-    [ trivial with arith
-      | rewrite Zmult_comm; rewrite Zmult_1_l; rewrite Zplus_0_r;
-	unfold Zle in |- *; elim x; intros; simpl in |- *; 
-          discriminate ].
+  intros x y H.
+  destruct (le_lt_dec y x) as [H0|H0]; auto.
+  elimtype False.
+  assert (H1:=inj_gt _ _ H0).
+  red in H; red in H1.
+  rewrite <- Zcompare_antisym in H; rewrite H1 in H; auto.
+Qed.
+
+Theorem inj_gt_rev : forall n m:nat, Z_of_nat n > Z_of_nat m -> (n > m)%nat.
+Proof.
+  intros x y H.
+  destruct (le_lt_dec x y) as [H0|H0]; auto.
+  elimtype False.
+  assert (H1:=inj_ge _ _ H0).
+  red in H; red in H1.
+  rewrite <- Zcompare_antisym in H1; rewrite H in H1; auto.
+Qed.
+
+(* Both ways ... *)
+
+Theorem inj_le_iff : forall n m:nat, (n<=m)%nat <-> Z_of_nat n <= Z_of_nat m.
+Proof.
+ split; [apply inj_le | apply inj_le_rev].
+Qed.
+
+Theorem inj_lt_iff : forall n m:nat, (n<m)%nat <-> Z_of_nat n < Z_of_nat m.
+Proof.
+ split; [apply inj_lt | apply inj_lt_rev].
+Qed.
+
+Theorem inj_ge_iff : forall n m:nat, (n>=m)%nat <-> Z_of_nat n >= Z_of_nat m.
+Proof.
+ split; [apply inj_ge | apply inj_ge_rev].
+Qed.
+
+Theorem inj_gt_iff : forall n m:nat, (n>m)%nat <-> Z_of_nat n > Z_of_nat m.
+Proof.
+ split; [apply inj_gt | apply inj_gt_rev].
+Qed.
+
+(** Injection and usual operations *)
+ 
+Theorem inj_plus : forall n m:nat, Z_of_nat (n + m) = Z_of_nat n + Z_of_nat m.
+Proof.
+  intro x; induction x as [| n H]; intro y; destruct y as [| m];
+    [ simpl in |- *; trivial with arith
+      | simpl in |- *; trivial with arith
+      | simpl in |- *; rewrite <- plus_n_O; trivial with arith
+      | change (Z_of_nat (S (n + S m)) = Z_of_nat (S n) + Z_of_nat (S m)) in |- *;
+	rewrite inj_S; rewrite H; do 2 rewrite inj_S; rewrite Zplus_succ_l;
+	  trivial with arith ].
+Qed.
+
+Theorem inj_mult : forall n m:nat, Z_of_nat (n * m) = Z_of_nat n * Z_of_nat m.
+Proof.
+  intro x; induction x as [| n H];
+    [ simpl in |- *; trivial with arith
+      | intro y; rewrite inj_S; rewrite <- Zmult_succ_l_reverse; rewrite <- H;
+	rewrite <- inj_plus; simpl in |- *; rewrite plus_comm; 
+	  trivial with arith ].
 Qed.
 
 Theorem inj_minus1 :
@@ -121,6 +200,46 @@ Proof.
     [ trivial with arith | apply gt_not_le; assumption ].
 Qed.
 
+Theorem inj_minus : forall n m:nat, 
+ Z_of_nat (minus n m) = Zmax 0 (Z_of_nat n - Z_of_nat m).
+Proof.
+ intros.
+ rewrite Zmax_comm.
+ unfold Zmax.
+ destruct (le_lt_dec m n) as [H|H].
+
+ rewrite (inj_minus1 _ _ H).
+ assert (H':=Zle_minus_le_0 _ _ (inj_le _ _ H)).
+ unfold Zle in H'.
+ rewrite <- Zcompare_antisym in H'.
+ destruct Zcompare; simpl in *; intuition.
+
+ rewrite (inj_minus2 _ _ H).
+ assert (H':=Zplus_lt_compat_r _ _ (- Z_of_nat m) (inj_lt _ _ H)).
+ rewrite Zplus_opp_r in H'.
+ unfold Zminus; rewrite H'; auto.
+Qed.
+
+Theorem inj_min : forall n m:nat, 
+  Z_of_nat (min n m) = Zmin (Z_of_nat n) (Z_of_nat m).
+Proof.
+ induction n; destruct m; try (compute; auto; fail).
+ simpl min.
+ do 3 rewrite inj_S.
+ rewrite <- Zsucc_min_distr; f_equal; auto.
+Qed.
+
+Theorem inj_max : forall n m:nat, 
+  Z_of_nat (max n m) = Zmax (Z_of_nat n) (Z_of_nat m).
+Proof.
+ induction n; destruct m; try (compute; auto; fail).
+ simpl max.
+ do 3 rewrite inj_S.
+ rewrite <- Zsucc_max_distr; f_equal; auto.
+Qed.
+
+(** Composition of injections **)
+
 Theorem Zpos_eq_Z_of_nat_o_nat_of_P :
   forall p:positive, Zpos p = Z_of_nat (nat_of_P p).
 Proof.
@@ -136,3 +255,31 @@ Proof.
   rewrite inj_plus; repeat rewrite <- H.
   rewrite Zpos_xO; simpl in |- *; rewrite Pplus_diag; reflexivity.
 Qed.
+
+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.
+
+(** Misc *)
+
+Theorem intro_Z :
+  forall n:nat,  exists y : Z, Z_of_nat n = y /\ 0 <= y * 1 + 0.
+Proof.
+  intros x; exists (Z_of_nat x); split;
+    [ trivial with arith
+      | rewrite Zmult_comm; rewrite Zmult_1_l; rewrite Zplus_0_r;
+	unfold Zle in |- *; elim x; intros; simpl in |- *; 
+          discriminate ].
+Qed.
+
+Lemma Zpos_P_of_succ_nat : forall n:nat, 
+ Zpos (P_of_succ_nat n) = Zsucc (Z_of_nat n).
+Proof.
+  intros.
+  unfold Z_of_nat.
+  destruct n.
+  simpl; auto.
+  simpl (P_of_succ_nat (S n)).
+  apply Zpos_succ_morphism.
+Qed.