A generic preprocessing tactic zify for (r)omega

------------------------------------------------ 

See file PreOmega for more details and/or test-suite/succes/*Omega*.v

The zify tactic performs a Z-ification of your current goal,
transforming parts of type nat, N, positive, taking advantage of many
equivalences of operations, and of the positivity implied by these
types.

Integration with omega and romega:
 (r)omega : the earlier tactics, 100% compatible 
 (r)omega with * : full zify applied before the (r)omega run
 (r)omega with <types>, where <types> is a sub-list of {nat,N,positive,Z}, 
   applies only specific parts of zify (btw "with Z" means take advantage 
   of Zmax, Zmin, Zabs and Zsgn). 

As a particular consequence, "romega with nat" should now be a
close-to-perfect replacement for omega. Slightly more powerful, since
(forall x:nat, x*x>=0) is provable and also slightly less powerful: if
False is somewhere in the hypothesis, it doesn't use it. 

For the moment zify is done in a direct way in Ltac, using rewrite
when necessary, but crucial chains of rewrite may be made reflexive
some day.

Even though zify is designed to help (r)omega, I think it might be 
of interest for other tactics (micromega ?). Feel free to complete
zify if your favorite operation / type isn't handled yet. 


Side-effects: 

- additional results for ZArith, NArith, etc...
- definition of Ple, Plt, Pgt, Pge and notations for them in positive_scope
- romega now start by doing "intros". Since the conclusion will be negated, 
  and this operation will be justified by means of decidability, it helps
  to have as little as possible in the conclusion. 






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

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.