Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

6 files changed, 1873 insertions, 1237 deletions

diff --git a/contrib/romega/ROmega.v b/contrib/romega/ROmega.v
index 19933873..68bc43bb 100644
--- a/contrib/romega/ROmega.v
+++ b/contrib/romega/ROmega.v
@@ -1,10 +1,11 @@
 (*************************************************************************
 
    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 Setoid.
+Require Export PreOmega.
diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v
index d20cafc1..9d379548 100644
--- a/contrib/romega/ReflOmegaCore.v
+++ b/contrib/romega/ReflOmegaCore.v
@@ -7,32 +7,852 @@
 
  *************************************************************************)
 
-Require Import Arith.
-Require Import List.
-Require Import Bool.
-Require Import ZArith_base.
-Require Import OmegaLemmas.
-
-Open Scope Z_scope.
-
-(* \subsection{Definition of basic types} *)
-
-(* \subsubsection{Environment of propositions (lists) *)
-Inductive PropList : Type :=
-  | Pnil : PropList
-  | Pcons : Prop -> PropList -> PropList.
-
-(* Access function for the environment with a default *)
-Fixpoint nthProp (n : nat) (l : PropList) (default : Prop) {struct l} :
- Prop :=
-  match n, l with
-  | O, Pcons x l' => x
-  | O, other => default
-  | S m, Pnil => default
-  | S m, Pcons x t => nthProp m t default
-  end.
+Require Import List Bool Sumbool EqNat Setoid Ring_theory Decidable.
+Delimit Scope Int_scope with I.
+
+(* Abstract Integers. *)
+
+Module Type Int. 
+
+  Parameter int : Set. 
+
+  Parameter zero : int. 
+  Parameter one : int. 
+  Parameter plus : int -> int -> int. 
+  Parameter opp : int -> int.
+  Parameter minus : int -> int -> int. 
+  Parameter mult : int -> int -> int.
+
+  Notation "0" := zero : Int_scope.
+  Notation "1" := one : Int_scope. 
+  Infix "+" := plus : Int_scope.
+  Infix "-" := minus : Int_scope.
+  Infix "*" := mult : Int_scope.
+  Notation "- x" := (opp x) : Int_scope.
+
+  Open Scope Int_scope.
+
+  (* First, int is a ring: *)
+  Axiom ring : @ring_theory int 0 1 plus mult minus opp (@eq int).
+
+  (* int should also be ordered: *)
+
+  Parameter le : int -> int -> Prop.
+  Parameter lt : int -> int -> Prop.
+  Parameter ge : int -> int -> Prop.
+  Parameter gt : int -> int -> Prop.
+  Notation "x <= y" := (le x y): Int_scope.
+  Notation "x < y" := (lt x y) : Int_scope.
+  Notation "x >= y" := (ge x y) : Int_scope.
+  Notation "x > y" := (gt x y): Int_scope.
+  Axiom le_lt_iff : forall i j, (i<=j) <-> ~(j<i).
+  Axiom ge_le_iff : forall i j, (i>=j) <-> (j<=i).
+  Axiom gt_lt_iff : forall i j, (i>j) <-> (j<i).
+
+  (* Basic properties of this order *)
+  Axiom lt_trans : forall i j k, i<j -> j<k -> i<k.
+  Axiom lt_not_eq : forall i j, i<j -> i<>j.
+
+  (* Compatibilities *)
+  Axiom lt_0_1 : 0<1.
+  Axiom plus_le_compat : forall i j k l, i<=j -> k<=l -> i+k<=j+l.
+  Axiom opp_le_compat : forall i j, i<=j -> (-j)<=(-i).
+  Axiom mult_lt_compat_l : 
+   forall i j k, 0 < k -> i < j -> k*i<k*j.
+
+  (* We should have a way to decide the equality and the order*)  
+  Parameter compare : int -> int -> comparison.
+  Infix "?=" := compare (at level 70, no associativity) : Int_scope.
+  Axiom compare_Eq : forall i j, compare i j = Eq <-> i=j.
+  Axiom compare_Lt : forall i j, compare i j = Lt <-> i<j.
+  Axiom compare_Gt : forall i j, compare i j = Gt <-> i>j.
+
+  (* Up to here, these requirements could be fulfilled 
+     by any totally ordered ring. Let's now be int-specific: *)
+  Axiom le_lt_int : forall x y, x<y <-> x<=y+-(1).
+
+  (* Btw, lt_0_1 could be deduced from this last axiom *)
+
+End Int.
+
+
+
+(* Of course, Z is a model for our abstract int *)
+
+Module Z_as_Int <: Int.
+
+  Require Import ZArith_base.
+  Open Scope Z_scope.
+
+  Definition int := Z. 
+  Definition zero := 0. 
+  Definition one := 1. 
+  Definition plus := Zplus.
+  Definition opp := Zopp.
+  Definition minus := Zminus.
+  Definition mult := Zmult.
+
+  Lemma ring : @ring_theory int zero one plus mult minus opp (@eq int).
+  Proof.
+  constructor.
+  exact Zplus_0_l.
+  exact Zplus_comm.
+  exact Zplus_assoc.
+  exact Zmult_1_l.
+  exact Zmult_comm.
+  exact Zmult_assoc.
+  exact Zmult_plus_distr_l.
+  unfold minus, Zminus; auto.
+  exact Zplus_opp_r.
+  Qed.
+
+  Definition le := Zle.
+  Definition lt := Zlt.
+  Definition ge := Zge.
+  Definition gt := Zgt.
+  Lemma le_lt_iff : forall i j, (i<=j) <-> ~(j<i).
+  Proof.
+   split; intros.
+   apply Zle_not_lt; auto.
+   rewrite <- Zge_iff_le.
+   apply Znot_lt_ge; auto.
+  Qed.
+  Definition ge_le_iff := Zge_iff_le.
+  Definition gt_lt_iff := Zgt_iff_lt.
+
+  Definition lt_trans := Zlt_trans.
+  Definition lt_not_eq := Zlt_not_eq.
+
+  Definition lt_0_1 := Zlt_0_1.
+  Definition plus_le_compat := Zplus_le_compat.
+  Definition mult_lt_compat_l := Zmult_lt_compat_l.
+  Lemma opp_le_compat : forall i j, i<=j -> (-j)<=(-i).
+  Proof.
+  unfold Zle; intros; rewrite <- Zcompare_opp; auto.
+  Qed.
+
+  Definition compare := Zcompare.
+  Definition compare_Eq := Zcompare_Eq_iff_eq.
+  Lemma compare_Lt : forall i j, compare i j = Lt <-> i<j.
+  Proof. intros; unfold compare, Zlt; intuition. Qed.
+  Lemma compare_Gt : forall i j, compare i j = Gt <-> i>j.
+  Proof. intros; unfold compare, Zgt; intuition. Qed.
+
+  Lemma le_lt_int : forall x y, x<y <-> x<=y+-(1).
+  Proof.
+   intros; split; intros.
+   generalize (Zlt_left _ _ H); simpl; intros.
+   apply Zle_left_rev; auto.
+   apply Zlt_0_minus_lt.
+   generalize (Zplus_le_lt_compat x (y+-1) (-x) (-x+1) H).
+   rewrite Zplus_opp_r.
+   rewrite <-Zplus_assoc.
+   rewrite (Zplus_permute (-1)).
+   simpl in *.
+   rewrite Zplus_0_r.
+   intro H'; apply H'.
+   replace (-x+1) with (Zsucc (-x)); auto.
+   apply Zlt_succ.
+  Qed.
+
+End Z_as_Int.  
+
+
+
+
+Module IntProperties (I:Int). 
+ Import I.
+ 
+ (* Primo, some consequences of being a ring theory... *)
+ 
+ Definition two := 1+1.
+ Notation "2" := two : Int_scope. 
+
+ (* Aliases for properties packed in the ring record. *)
+
+ Definition plus_assoc := ring.(Radd_assoc).
+ Definition plus_comm := ring.(Radd_comm).
+ Definition plus_0_l := ring.(Radd_0_l).
+ Definition mult_assoc := ring.(Rmul_assoc). 
+ Definition mult_comm := ring.(Rmul_comm).
+ Definition mult_1_l := ring.(Rmul_1_l).
+ Definition mult_plus_distr_r := ring.(Rdistr_l).
+ Definition opp_def := ring.(Ropp_def).
+ Definition minus_def := ring.(Rsub_def).
+
+ Opaque plus_assoc plus_comm plus_0_l mult_assoc mult_comm mult_1_l 
+  mult_plus_distr_r opp_def minus_def.
+
+ (* More facts about plus *)
+
+ Lemma plus_0_r : forall x, x+0 = x.
+ Proof. intros; rewrite plus_comm; apply plus_0_l. Qed.
+
+ Lemma plus_0_r_reverse : forall x, x = x+0.
+ Proof. intros; symmetry; apply plus_0_r. Qed. 
+
+ Lemma plus_assoc_reverse : forall x y z, x+y+z = x+(y+z).
+ Proof. intros; symmetry; apply plus_assoc. Qed.
+
+ Lemma plus_permute : forall x y z, x+(y+z) = y+(x+z).
+ Proof. intros; do 2 rewrite plus_assoc; f_equal; apply plus_comm. Qed.
+
+ Lemma plus_reg_l : forall x y z, x+y = x+z -> y = z.
+ Proof. 
+  intros.
+  rewrite (plus_0_r_reverse y), (plus_0_r_reverse z), <-(opp_def x).
+  now rewrite plus_permute, plus_assoc, H, <- plus_assoc, plus_permute. 
+ Qed.
+
+ (* More facts about mult *) 
+   
+ Lemma mult_assoc_reverse : forall x y z, x*y*z = x*(y*z).
+ Proof. intros; symmetry; apply mult_assoc. Qed.
+
+ Lemma mult_plus_distr_l : forall x y z, x*(y+z)=x*y+x*z.
+ Proof.
+  intros.
+  rewrite (mult_comm x (y+z)), (mult_comm x y), (mult_comm x z).
+  apply mult_plus_distr_r.
+ Qed.
+
+ Lemma mult_0_l : forall x, 0*x = 0.
+ Proof. 
+  intros.
+  generalize (mult_plus_distr_r 0 1 x).
+  rewrite plus_0_l, mult_1_l, plus_comm; intros.
+  apply plus_reg_l with x.
+  rewrite <- H.
+  apply plus_0_r_reverse.
+ Qed.
+ 
+
+ (* More facts about opp *)
+
+ Definition plus_opp_r := opp_def.
+
+ Lemma plus_opp_l : forall x, -x + x = 0.
+ Proof. intros; now rewrite plus_comm, opp_def. Qed.
+
+ Lemma mult_opp_comm : forall x y, - x * y = x * - y.
+ Proof.
+  intros.
+  apply plus_reg_l with (x*y).
+  rewrite <- mult_plus_distr_l, <- mult_plus_distr_r.
+  now rewrite opp_def, opp_def, mult_0_l, mult_comm, mult_0_l.
+ Qed.
+
+ Lemma opp_eq_mult_neg_1 : forall x, -x = x * -(1).
+ Proof.
+  intros; now rewrite mult_comm, mult_opp_comm, mult_1_l.
+ Qed.
+
+ Lemma opp_involutive : forall x, -(-x) = x.
+ Proof.
+  intros.
+  apply plus_reg_l with (-x).
+  now rewrite opp_def, plus_comm, opp_def.
+ Qed.
+
+ Lemma opp_plus_distr : forall x y, -(x+y) = -x + -y.
+ Proof.
+  intros.
+  apply plus_reg_l with (x+y).
+  rewrite opp_def.
+  rewrite plus_permute.
+  do 2 rewrite plus_assoc.
+  now rewrite (plus_comm (-x)), opp_def, plus_0_l, opp_def.
+ Qed.
+
+ Lemma opp_mult_distr_r : forall x y, -(x*y) = x * -y.
+ Proof.
+  intros.
+  rewrite <- mult_opp_comm.
+  apply plus_reg_l with (x*y).
+  now rewrite opp_def, <-mult_plus_distr_r, opp_def, mult_0_l.
+ Qed.  
+
+ Lemma egal_left : forall n m, n=m -> n+-m = 0.
+ Proof. intros; subst; apply opp_def. Qed.
+
+ Lemma ne_left_2 : forall x y : int, x<>y -> 0<>(x + - y).
+ Proof.
+ intros; contradict H.
+ apply (plus_reg_l (-y)).
+ now rewrite plus_opp_l, plus_comm, H.
+ Qed.
+
+ (* Special lemmas for factorisation. *)
+
+ Lemma red_factor0 : forall n, n = n*1.
+ Proof. symmetry; rewrite mult_comm; apply mult_1_l. Qed.
+
+ Lemma red_factor1 : forall n, n+n = n*2.
+ Proof. 
+  intros; unfold two.
+  now rewrite mult_comm, mult_plus_distr_r, mult_1_l.
+ Qed.
+
+ Lemma red_factor2 : forall n m, n + n*m = n * (1+m).
+ Proof.
+  intros; rewrite mult_plus_distr_l.
+  f_equal; now rewrite mult_comm, mult_1_l.
+ Qed.
+
+ Lemma red_factor3 : forall n m, n*m + n = n*(1+m).
+ Proof. intros; now rewrite plus_comm, red_factor2. Qed.
+
+ Lemma red_factor4 : forall n m p, n*m + n*p = n*(m+p).
+ Proof. 
+  intros; now rewrite mult_plus_distr_l.
+ Qed.
+ 
+ Lemma red_factor5 : forall n m , n * 0 + m = m.
+ Proof. intros; now rewrite mult_comm, mult_0_l, plus_0_l. Qed.
+
+ Definition red_factor6 := plus_0_r_reverse.
+
+
+ (* Specialized distributivities *)
+
+ Hint Rewrite mult_plus_distr_l mult_plus_distr_r mult_assoc : int.
+ Hint Rewrite <- plus_assoc : int.
+
+ Lemma OMEGA10 :
+  forall v c1 c2 l1 l2 k1 k2 : int,
+  (v * c1 + l1) * k1 + (v * c2 + l2) * k2 =
+  v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2).
+ Proof.
+  intros; autorewrite with int; f_equal; now rewrite plus_permute.
+ Qed.
+
+ Lemma OMEGA11 :
+  forall v1 c1 l1 l2 k1 : int,
+  (v1 * c1 + l1) * k1 + l2 = v1 * (c1 * k1) + (l1 * k1 + l2).
+ Proof.
+  intros; now autorewrite with int.
+ Qed.
+
+ Lemma OMEGA12 :
+  forall v2 c2 l1 l2 k2 : int,
+  l1 + (v2 * c2 + l2) * k2 = v2 * (c2 * k2) + (l1 + l2 * k2).
+ Proof.
+  intros; autorewrite with int; now rewrite plus_permute.
+ Qed.
+
+ Lemma OMEGA13 :
+  forall v l1 l2 x : int,
+  v * -x + l1 + (v * x + l2) = l1 + l2.
+ Proof.
+ intros; autorewrite with int.
+ rewrite plus_permute; f_equal.
+ rewrite plus_assoc.
+ now rewrite <- mult_plus_distr_l, plus_opp_l, mult_comm, mult_0_l, plus_0_l.
+ Qed.
+
+ Lemma OMEGA15 :
+  forall v c1 c2 l1 l2 k2 : int,
+  v * c1 + l1 + (v * c2 + l2) * k2 = v * (c1 + c2 * k2) + (l1 + l2 * k2).
+ Proof.
+  intros; autorewrite with int; f_equal; now rewrite plus_permute.
+ Qed.
+
+ Lemma OMEGA16 : forall v c l k : int, (v * c + l) * k = v * (c * k) + l * k.
+ Proof.
+  intros; now autorewrite with int.
+ Qed.
+
+ Lemma sum1 : forall a b c d : int, 0 = a -> 0 = b -> 0 = a * c + b * d.
+ Proof.
+ intros; elim H; elim H0; simpl in |- *; auto.
+ now rewrite mult_0_l, mult_0_l, plus_0_l.
+ Qed.
+
+
+ (* Secondo, some results about order (and equality) *)  
+
+ Lemma lt_irrefl : forall n, ~ n<n.
+ Proof.
+ intros n H.
+ elim (lt_not_eq _ _ H); auto.
+ Qed.
+
+ Lemma lt_antisym : forall n m, n<m -> m<n -> False.
+ Proof.
+ intros; elim (lt_irrefl _ (lt_trans _ _ _ H H0)); auto.
+ Qed.
+
+ Lemma lt_le_weak : forall n m, n<m -> n<=m.
+ Proof.
+  intros; rewrite le_lt_iff; intro H'; eapply lt_antisym; eauto.
+ Qed.
+
+ Lemma le_refl : forall n, n<=n.
+ Proof.
+ intros; rewrite le_lt_iff; apply lt_irrefl; auto.
+ Qed.
+
+ Lemma le_antisym : forall n m, n<=m -> m<=n -> n=m.
+ Proof.
+ intros n m; do 2 rewrite le_lt_iff; intros.
+ rewrite <- compare_Lt in H0.
+ rewrite <- gt_lt_iff, <- compare_Gt in H.
+ rewrite <- compare_Eq.
+ destruct compare; intuition.
+ Qed.
+
+ Lemma lt_eq_lt_dec : forall n m, { n<m }+{ n=m }+{ m<n }.
+ Proof.
+  intros.
+  generalize (compare_Lt n m)(compare_Eq n m)(compare_Gt n m).
+  destruct compare; [ left; right | left; left | right ]; intuition.
+  rewrite gt_lt_iff in H1; intuition.
+ Qed.
+
+ Lemma lt_dec : forall n m: int, { n<m } + { ~n<m }.
+ Proof.
+  intros.
+  generalize (compare_Lt n m)(compare_Eq n m)(compare_Gt n m).
+  destruct compare; [ right | left | right ]; intuition discriminate.
+ Qed.
+
+ Lemma lt_le_iff : forall n m, (n<m) <-> ~(m<=n).
+ Proof.
+  intros.
+  rewrite le_lt_iff.
+  destruct (lt_dec n m); intuition.
+ Qed.
+
+ Lemma le_dec : forall n m: int, { n<=m } + { ~n<=m }.
+ Proof.
+  intros; destruct (lt_dec m n); [right|left]; rewrite le_lt_iff; intuition.
+ Qed.
+
+ Lemma le_lt_dec : forall n m, { n<=m } + { m<n }.
+ Proof.
+  intros; destruct (le_dec n m); [left|right]; auto; now rewrite lt_le_iff.
+ Qed.
+
+
+ Definition beq i j := match compare i j with Eq => true | _ => false end.
+
+ Lemma beq_iff : forall i j, beq i j = true <-> i=j.
+ Proof.
+ intros; unfold beq; generalize (compare_Eq i j).
+ destruct compare; intuition discriminate.
+ Qed.
+                               
+ Lemma beq_true : forall i j, beq i j = true -> i=j.
+ Proof.
+ intros.
+ rewrite <- beq_iff; auto.
+ Qed.
+
+ Lemma beq_false : forall i j, beq i j = false -> i<>j.
+ Proof.
+ intros.
+ intro H'.
+ rewrite <- beq_iff in H'; rewrite H' in H; discriminate.
+ Qed.
+
+ Lemma eq_dec : forall n m:int, { n=m } + { n<>m }.
+ Proof.
+  intros; generalize (beq_iff n m); destruct beq; [left|right]; intuition.
+ Qed.
+
+ Definition bgt i j := match compare i j with Gt => true | _ => false end.
+
+ Lemma bgt_iff : forall i j, bgt i j = true <-> i>j.
+ Proof.
+ intros; unfold bgt; generalize (compare_Gt i j).
+ destruct compare; intuition discriminate.
+ Qed.
+
+ Lemma bgt_true : forall i j, bgt i j = true -> i>j.
+ Proof. intros; now rewrite <- bgt_iff. Qed.
+
+ Lemma bgt_false : forall i j, bgt i j = false -> i<=j.
+ Proof. 
+  intros.
+  rewrite le_lt_iff, <-gt_lt_iff, <-bgt_iff; intro H'; now rewrite H' in H.
+ Qed.
+
+ Lemma le_is_lt_or_eq : forall n m, n<=m -> { n<m } + { n=m }.
+ Proof.
+  intros.
+  destruct (eq_dec n m) as [H'|H'].
+  right; intuition.
+  left; rewrite lt_le_iff.
+  contradict H'.
+  apply le_antisym; auto.
+ Qed.
+
+ Lemma le_neq_lt : forall n m, n<=m -> n<>m -> n<m.
+ Proof.
+  intros.
+  destruct (le_is_lt_or_eq _ _ H); intuition.
+ Qed.
+
+ Lemma le_trans : forall n m p, n<=m -> m<=p -> n<=p.
+ Proof.
+  intros n m p; do 3 rewrite le_lt_iff; intros A B C.
+  destruct (lt_eq_lt_dec p m) as [[H|H]|H]; subst; auto.
+  generalize (lt_trans _ _ _ H C); intuition.
+ Qed.
+ 
+ (* order and operations *)
+
+ Lemma le_0_neg : forall n, 0 <= n <-> -n <= 0.
+ Proof.
+ intros.
+ pattern 0 at 2; rewrite <- (mult_0_l (-(1))).
+ rewrite <- opp_eq_mult_neg_1.
+ split; intros.
+ apply opp_le_compat; auto.
+ rewrite <-(opp_involutive 0), <-(opp_involutive n).
+ apply opp_le_compat; auto.
+ Qed.
+
+ Lemma le_0_neg' : forall n, n <= 0 <-> 0 <= -n.
+ Proof.
+ intros; rewrite le_0_neg, opp_involutive; intuition.
+ Qed.
+
+ Lemma plus_le_reg_r : forall n m p, n + p <= m + p -> n <= m.
+ Proof.
+ intros.
+ replace n with ((n+p)+-p).
+ replace m with ((m+p)+-p).
+ apply plus_le_compat; auto.
+ apply le_refl.
+ now rewrite <- plus_assoc, opp_def, plus_0_r.
+ now rewrite <- plus_assoc, opp_def, plus_0_r.
+ Qed.
+
+ Lemma plus_le_lt_compat : forall n m p q, n<=m -> p<q -> n+p<m+q.
+ Proof.
+ intros.
+ apply le_neq_lt.
+ apply plus_le_compat; auto.
+ apply lt_le_weak; auto.
+ rewrite lt_le_iff in H0.
+ contradict H0.
+ apply plus_le_reg_r with m.
+ rewrite (plus_comm q m), <-H0, (plus_comm p m).
+ apply plus_le_compat; auto.
+ apply le_refl; auto.
+ Qed.
+
+ Lemma plus_lt_compat : forall n m p q, n<m -> p<q -> n+p<m+q.
+ Proof.
+ intros.
+ apply plus_le_lt_compat; auto.
+ apply lt_le_weak; auto.
+ Qed.
+
+ Lemma opp_lt_compat : forall n m, n<m -> -m < -n.
+ Proof.
+ intros n m; do 2 rewrite lt_le_iff; intros H; contradict H.
+ rewrite <-(opp_involutive m), <-(opp_involutive n).
+ apply opp_le_compat; auto.
+ Qed.
+
+ Lemma lt_0_neg : forall n, 0 < n <-> -n < 0.
+ Proof.
+ intros.
+ pattern 0 at 2; rewrite <- (mult_0_l (-(1))).
+ rewrite <- opp_eq_mult_neg_1.
+ split; intros.
+ apply opp_lt_compat; auto.
+ rewrite <-(opp_involutive 0), <-(opp_involutive n).
+ apply opp_lt_compat; auto.
+ Qed.
+
+ Lemma lt_0_neg' : forall n, n < 0 <-> 0 < -n.
+ Proof.
+ intros; rewrite lt_0_neg, opp_involutive; intuition.
+ Qed.
+
+ Lemma mult_lt_0_compat : forall n m, 0 < n -> 0 < m -> 0 < n*m.
+ Proof.
+ intros.
+ rewrite <- (mult_0_l n), mult_comm.
+ apply mult_lt_compat_l; auto.
+ Qed.
+
+ Lemma mult_integral : forall n m, n * m = 0 -> n = 0 \/ m = 0.
+ Proof.
+ intros.
+ destruct (lt_eq_lt_dec n 0) as [[Hn|Hn]|Hn]; auto; 
+  destruct (lt_eq_lt_dec m 0) as [[Hm|Hm]|Hm]; auto; elimtype False.
+
+ rewrite lt_0_neg' in Hn.
+ rewrite lt_0_neg' in Hm.
+ generalize (mult_lt_0_compat _ _ Hn Hm).
+ rewrite <- opp_mult_distr_r, mult_comm, <- opp_mult_distr_r, opp_involutive.
+ rewrite mult_comm, H.
+ exact (lt_irrefl 0).
+
+ rewrite lt_0_neg' in Hn.
+ generalize (mult_lt_0_compat _ _ Hn Hm).
+ rewrite mult_comm, <- opp_mult_distr_r, mult_comm.
+ rewrite H.
+ rewrite opp_eq_mult_neg_1, mult_0_l.
+ exact (lt_irrefl 0).
+
+ rewrite lt_0_neg' in Hm.
+ generalize (mult_lt_0_compat _ _ Hn Hm).
+ rewrite <- opp_mult_distr_r.
+ rewrite H.
+ rewrite opp_eq_mult_neg_1, mult_0_l.
+ exact (lt_irrefl 0).
+
+ generalize (mult_lt_0_compat _ _ Hn Hm).
+ rewrite H.
+ exact (lt_irrefl 0).
+ Qed.
+
+ Lemma mult_le_compat : 
+   forall i j k l, i<=j -> k<=l -> 0<=i -> 0<=k -> i*k<=j*l.
+ Proof.
+ intros.
+ destruct (le_is_lt_or_eq _ _ H1).
+
+ apply le_trans with (i*l).
+ destruct (le_is_lt_or_eq _ _ H0); [ | subst; apply le_refl].
+ apply lt_le_weak.
+ apply mult_lt_compat_l; auto.
+
+ generalize (le_trans _ _ _ H2 H0); clear H0 H1 H2; intros.
+ rewrite (mult_comm i), (mult_comm j).
+ destruct (le_is_lt_or_eq _ _ H0); 
+  [ | subst; do 2 rewrite mult_0_l; apply le_refl].
+ destruct (le_is_lt_or_eq _ _ H); 
+  [ | subst; apply le_refl].
+ apply lt_le_weak.
+ apply mult_lt_compat_l; auto.
+
+ subst i.
+ rewrite mult_0_l.
+ generalize (le_trans _ _ _ H2 H0); clear H0 H1 H2; intros.
+ destruct (le_is_lt_or_eq _ _ H); 
+  [ | subst; rewrite mult_0_l; apply le_refl].
+ destruct (le_is_lt_or_eq _ _ H0); 
+  [ | subst; rewrite mult_comm, mult_0_l; apply le_refl].
+ apply lt_le_weak.
+ apply mult_lt_0_compat; auto.
+ Qed.
+
+ Lemma sum5 :
+ forall a b c d : int, c <> 0 -> 0 <> a -> 0 = b -> 0 <> a * c + b * d.
+ Proof.
+ intros.
+ subst b; rewrite mult_0_l, plus_0_r.
+ contradict H.
+ symmetry in H; destruct (mult_integral _ _ H); congruence.
+ Qed.
+
+ Lemma one_neq_zero : 1 <> 0.
+ Proof.
+ red; intro.
+ symmetry in H.
+ apply (lt_not_eq 0 1); auto.
+ apply lt_0_1.
+ Qed.
+
+ Lemma minus_one_neq_zero : -(1) <> 0.
+ Proof.
+ apply lt_not_eq.
+ rewrite <- lt_0_neg.
+ apply lt_0_1.
+ Qed.
+
+ Lemma le_left : forall n m, n <= m -> 0 <= m + - n.
+ Proof.
+  intros.
+  rewrite <- (opp_def m).
+  apply plus_le_compat.
+  apply le_refl.
+  apply opp_le_compat; auto.
+ Qed.
+
+ Lemma OMEGA2 : forall x y, 0 <= x -> 0 <= y -> 0 <= x + y.
+ Proof.
+ intros.
+ replace 0 with (0+0).
+ apply plus_le_compat; auto.
+ rewrite plus_0_l; auto.
+ Qed.
+
+ Lemma OMEGA8 : forall x y, 0 <= x -> 0 <= y -> x = - y -> x = 0.
+ Proof.
+ intros.
+ assert (y=-x).
+  subst x; symmetry; apply opp_involutive.
+ clear H1; subst y.
+ destruct (eq_dec 0 x) as [H'|H']; auto.
+ assert (H'':=le_neq_lt _ _ H H').
+ generalize (plus_le_lt_compat _ _ _ _ H0 H'').
+ rewrite plus_opp_l, plus_0_l.
+ intros.
+ elim (lt_not_eq _ _ H1); auto.
+ Qed.
+
+ Lemma sum2 :
+ forall a b c d : int, 0 <= d -> 0 = a -> 0 <= b -> 0 <= a * c + b * d.
+ Proof.
+ intros.
+ subst a; rewrite mult_0_l, plus_0_l.
+ rewrite <- (mult_0_l 0).
+ apply mult_le_compat; auto; apply le_refl.
+ Qed.
+
+ Lemma sum3 :
+ forall a b c d : int,
+  0 <= c -> 0 <= d -> 0 <= a -> 0 <= b -> 0 <= a * c + b * d.
+ Proof.
+ intros.
+ rewrite <- (plus_0_l 0).
+ apply plus_le_compat; auto.
+ rewrite <- (mult_0_l 0).
+ apply mult_le_compat; auto; apply le_refl.
+ rewrite <- (mult_0_l 0).
+ apply mult_le_compat; auto; apply le_refl.
+ Qed.
+
+ Lemma sum4 : forall k : int, k>0 -> 0 <= k.
+ Proof.
+ intros k; rewrite gt_lt_iff; apply lt_le_weak.
+ Qed.
+
+ (* Lemmas specific to integers (they use lt_le_int) *)
+
+ Lemma lt_left : forall n m, n < m -> 0 <= m + -(1) + - n.
+ Proof.
+ intros; apply le_left.
+ now rewrite <- le_lt_int.
+ Qed.
+
+ Lemma lt_left_inv : forall x y, 0 <= y + -(1) + - x -> x < y.
+ Proof.
+ intros.
+ generalize (plus_le_compat _ _ _ _ H (le_refl x)); clear H.
+ now rewrite plus_0_l, <-plus_assoc, plus_opp_l, plus_0_r, le_lt_int.
+ Qed.
+
+ Lemma OMEGA4 : forall x y z, x > 0 -> y > x -> z * y + x <> 0.
+ Proof.
+ intros.
+ intro H'.
+ rewrite gt_lt_iff in H,H0.
+ destruct (lt_eq_lt_dec z 0) as [[G|G]|G].
+
+ rewrite lt_0_neg' in G.
+ generalize (plus_le_lt_compat _ _ _ _ (le_refl (z*y)) H0).
+ rewrite H'.
+ pattern y at 2; rewrite <-(mult_1_l y), <-mult_plus_distr_r.
+ intros.
+ rewrite le_lt_int in G.
+ rewrite <- opp_plus_distr in G.
+ assert (0 < y) by (apply lt_trans with x; auto).
+ generalize (mult_le_compat _ _ _ _ G (lt_le_weak _ _ H2) (le_refl 0) (le_refl 0)).
+ rewrite mult_0_l, mult_comm, <- opp_mult_distr_r, mult_comm, <-le_0_neg', le_lt_iff.
+ intuition.
+
+ subst; rewrite mult_0_l, plus_0_l in H'; subst.
+ apply (lt_not_eq _ _ H); auto.
+
+ apply (lt_not_eq 0 (z*y+x)); auto.
+ rewrite <- (plus_0_l 0).
+ apply plus_lt_compat; auto.
+ apply mult_lt_0_compat; auto.
+ apply lt_trans with x; auto.
+ Qed. 
+
+ Lemma OMEGA19 : forall x, x<>0 -> 0 <= x + -(1) \/ 0 <= x * -(1) + -(1).
+ Proof.
+ intros.
+ do 2 rewrite <- le_lt_int.
+ rewrite <- opp_eq_mult_neg_1.
+ destruct (lt_eq_lt_dec 0 x) as [[H'|H']|H'].
+ auto.
+ congruence.
+ right.
+ rewrite <-(mult_0_l (-(1))), <-(opp_eq_mult_neg_1 0).
+ apply opp_lt_compat; auto.
+ Qed.
+
+ Lemma mult_le_approx : 
+  forall n m p, n > 0 -> n > p -> 0 <= m * n + p -> 0 <= m.
+ Proof.
+ intros n m p.
+ do 2 rewrite gt_lt_iff.
+ do 2 rewrite le_lt_iff; intros.
+ contradict H1.
+ rewrite lt_0_neg' in H1.
+ rewrite lt_0_neg'.
+ rewrite opp_plus_distr.
+ rewrite mult_comm, opp_mult_distr_r.
+ rewrite le_lt_int.
+ rewrite <- plus_assoc, (plus_comm (-p)), plus_assoc.
+ apply lt_left.
+ rewrite le_lt_int.
+ rewrite le_lt_int in H0.
+ apply le_trans with (n+-(1)); auto.
+ apply plus_le_compat; [ | apply le_refl ].
+ rewrite le_lt_int in H1.
+ generalize (mult_le_compat _ _ _ _ (lt_le_weak _ _ H) H1 (le_refl 0) (le_refl 0)).
+ rewrite mult_0_l.
+ rewrite mult_plus_distr_l.
+ rewrite <- opp_eq_mult_neg_1.
+ intros.
+ generalize (plus_le_compat _ _ _ _ (le_refl n) H2).
+ now rewrite plus_permute, opp_def, plus_0_r, plus_0_r.
+ Qed.
+
+ (* Some decidabilities *)
+
+ Lemma dec_eq : forall i j:int, decidable (i=j).
+ Proof.
+  red; intros; destruct (eq_dec i j); auto.
+ Qed.
+
+ Lemma dec_ne : forall i j:int, decidable (i<>j).
+ Proof.
+  red; intros; destruct (eq_dec i j); auto.
+ Qed.
+
+ Lemma dec_le : forall i j:int, decidable (i<=j).
+ Proof.
+  red; intros; destruct (le_dec i j); auto.
+ Qed.
+
+ Lemma dec_lt : forall i j:int, decidable (i<j).
+ Proof.
+  red; intros; destruct (lt_dec i j); auto.
+ Qed.
+
+ Lemma dec_ge : forall i j:int, decidable (i>=j).
+ Proof.
+  red; intros; rewrite ge_le_iff; destruct (le_dec j i); auto.
+ Qed.
+
+ Lemma dec_gt : forall i j:int, decidable (i>j).
+ Proof.
+  red; intros; rewrite gt_lt_iff; destruct (lt_dec j i); auto.
+ Qed.
+
+End IntProperties.
+
+
+
+
+Module IntOmega (I:Int).
+Import I.
+Module IP:=IntProperties(I).
+Import IP.
    
-(* \subsubsection{Définition of reified integer expressions}
+(* \subsubsection{Definition of reified integer expressions}
    Terms are either:
    \begin{itemize}
    \item integers [Tint]
@@ -41,7 +861,7 @@ Fixpoint nthProp (n : nat) (l : PropList) (default : Prop) {struct l} :
    The last two are translated in additions and products. *)
 
 Inductive term : Set :=
-  | Tint : Z -> term
+  | Tint : int -> term
   | Tplus : term -> term -> term
   | Tmult : term -> term -> term
   | Tminus : term -> term -> term
@@ -49,6 +869,7 @@ Inductive term : Set :=
   | Tvar : nat -> term.
 
 Delimit Scope romega_scope with term.
+Arguments Scope Tint [Int_scope].
 Arguments Scope Tplus [romega_scope romega_scope].
 Arguments Scope Tmult [romega_scope romega_scope].
 Arguments Scope Tminus [romega_scope romega_scope].
@@ -58,20 +879,21 @@ Infix "+" := Tplus : romega_scope.
 Infix "*" := Tmult : romega_scope.
 Infix "-" := Tminus : romega_scope.
 Notation "- x" := (Topp x) : romega_scope.
-Notation "[ x ]" := (Tvar x) (at level 1) : romega_scope.
+Notation "[ x ]" := (Tvar x) (at level 0) : romega_scope.
 
 (* \subsubsection{Definition of reified goals} *)
+
 (* Very restricted definition of handled predicates that should be extended
    to cover a wider set of operations.
    Taking care of negations and disequations require solving more than a
    goal in parallel. This is a major improvement over previous versions. *)
 
 Inductive proposition : Set :=
-  | EqTerm : term -> term -> proposition (* egalité entre termes *)
-  | LeqTerm : term -> term -> proposition (* plus petit ou egal *)
-  | TrueTerm : proposition (* vrai *)
-  | FalseTerm : proposition (* faux *)
-  | Tnot : proposition -> proposition (* négation *)
+  | EqTerm : term -> term -> proposition (* equality between terms *)
+  | LeqTerm : term -> term -> proposition (* less or equal on terms *)
+  | TrueTerm : proposition (* true *)
+  | FalseTerm : proposition (* false *)
+  | Tnot : proposition -> proposition (* negation *)
   | GeqTerm : term -> term -> proposition
   | GtTerm : term -> term -> proposition
   | LtTerm : term -> term -> proposition
@@ -87,7 +909,7 @@ Notation hyps := (list proposition).
 (* Definition of lists of subgoals  (set of open goals) *)
 Notation lhyps := (list hyps).
 
-(* a syngle goal packed in a subgoal list *)
+(* a single goal packed in a subgoal list *)
 Notation singleton := (fun a : hyps => a :: nil).
 
 (* an absurd goal *)
@@ -110,24 +932,22 @@ Inductive t_fusion : Set :=
 
 (* \subsubsection{Rewriting steps to normalize terms} *)
 Inductive step : Set := 
- (* apply the rewriting steps to both subterms of an operation *)
-  | C_DO_BOTH :
-      step -> step -> step
-              (* apply the rewriting step to the first branch *)
+  (* apply the rewriting steps to both subterms of an operation *)
+  | C_DO_BOTH : step -> step -> step
+  (* apply the rewriting step to the first branch *)
   | C_LEFT : step -> step
-             (* apply the rewriting step to the second branch *)
+  (* apply the rewriting step to the second branch *)
   | C_RIGHT : step -> step
-              (* apply two steps consecutively to a term *)
-  | C_SEQ : step -> step -> step
-                    (* empty step *)
-  | C_NOP : step
-      (* the following operations correspond to actual rewriting *)
+  (* apply two steps consecutively to a term *)
+  | C_SEQ : step -> step -> step 
+  (* empty step *)
+  | C_NOP : step 
+  (* the following operations correspond to actual rewriting *)
   | C_OPP_PLUS : step
   | C_OPP_OPP : step
   | C_OPP_MULT_R : step
-  | C_OPP_ONE :
-      step
-      (* This is a special step that reduces the term (computation) *)
+  | C_OPP_ONE : step
+  (* This is a special step that reduces the term (computation) *)
   | C_REDUCE : step
   | C_MULT_PLUS_DISTR : step
   | C_MULT_OPP_LEFT : step
@@ -152,261 +972,98 @@ Inductive step : Set :=
    the trace coming from the decision procedure Omega. *)
 
 Inductive t_omega : Set :=
- (* n = 0 n!= 0 *)
+  (* n = 0 and n!= 0 *)
   | O_CONSTANT_NOT_NUL : nat -> t_omega
-  | O_CONSTANT_NEG :
-      nat -> t_omega
-      (* division et approximation of an equation *)
-  | O_DIV_APPROX :
-      Z ->
-      Z ->
-      term ->
-      nat ->
-      t_omega -> nat -> t_omega
-                 (* no solution because no exact division *)
-  | O_NOT_EXACT_DIVIDE :
-      Z -> Z -> term -> nat -> nat -> t_omega
-                               (* exact division *)
-  | O_EXACT_DIVIDE : Z -> term -> nat -> t_omega -> nat -> t_omega
-  | O_SUM : Z -> nat -> Z -> nat -> list t_fusion -> t_omega -> t_omega
+  | O_CONSTANT_NEG : nat -> t_omega
+  (* division and approximation of an equation *)
+  | O_DIV_APPROX : int -> int -> term -> nat -> t_omega -> nat -> t_omega
+  (* no solution because no exact division *)
+  | O_NOT_EXACT_DIVIDE : int -> int -> term -> nat -> nat -> t_omega
+  (* exact division *)
+  | O_EXACT_DIVIDE : int -> term -> nat -> t_omega -> nat -> t_omega
+  | O_SUM : int -> nat -> int -> nat -> list t_fusion -> t_omega -> t_omega
   | O_CONTRADICTION : nat -> nat -> nat -> t_omega
   | O_MERGE_EQ : nat -> nat -> nat -> t_omega -> t_omega
   | O_SPLIT_INEQ : nat -> nat -> t_omega -> t_omega -> t_omega
   | O_CONSTANT_NUL : nat -> t_omega
   | O_NEGATE_CONTRADICT : nat -> nat -> t_omega
   | O_NEGATE_CONTRADICT_INV : nat -> nat -> nat -> t_omega
-  | O_STATE : Z -> step -> nat -> nat -> t_omega -> t_omega.
+  | O_STATE : int -> step -> nat -> nat -> t_omega -> t_omega.
+
+(* \subsubsection{Rules for normalizing the hypothesis} *)
+(* These rules indicate how to normalize useful propositions 
+   of each useful hypothesis before the decomposition of hypothesis. 
+   The rules include the inversion phase for negation removal. *)
 
-(* \subsubsection{Règles pour normaliser les hypothèses} *)
-(* Ces règles indiquent comment normaliser les propositions utiles 
-   de chaque hypothèse utile avant la décomposition des hypothèses et 
-   incluent l'étape d'inversion pour la suppression des négations *)
 Inductive p_step : Set :=
   | P_LEFT : p_step -> p_step
   | P_RIGHT : p_step -> p_step
   | P_INVERT : step -> p_step
   | P_STEP : step -> p_step
   | P_NOP : p_step.
-(* Liste des normalisations a effectuer : avec un constructeur dans le
-   type [p_step] permettant
-   de parcourir à la fois les branches gauches et droit, on pourrait n'avoir
-   qu'une normalisation par hypothèse. Et comme toutes les hypothèses sont 
-   utiles (sinon on ne les inclurait pas), on pourrait remplacer [h_step] 
-   par une simple liste *)
+
+(* List of normalizations to perform : with a constructor of type 
+   [p_step] allowing to visit both left and right branches, we would be  
+   able to restrict to only one normalization by hypothesis. 
+   And since all hypothesis are useful (otherwise they wouldn't be included), 
+   we would be able to replace [h_step] by a simple list. *)
 
 Inductive h_step : Set :=
     pair_step : nat -> p_step -> h_step.
 
-(* \subsubsection{Règles pour décomposer les hypothèses} *)
-(* Ce type permet de se diriger dans les constructeurs logiques formant les
-   prédicats des hypothèses pour aller les décomposer. Ils permettent
-   en particulier d'extraire une hypothèse d'une conjonction avec
-   éventuellement le bon niveau de négations. *)
+(* \subsubsection{Rules for decomposing the hypothesis} *)
+(* This type allows to navigate in the logical constructors that 
+   form the predicats of the hypothesis in order to decompose them. 
+   This allows in particular to extract one hypothesis from a 
+   conjonction with possibly the right level of negations. *)
 
 Inductive direction : Set :=
   | D_left : direction
   | D_right : direction
   | D_mono : direction.
 
-(* Ce type permet d'extraire les composants utiles des hypothèses : que ce
-   soit des hypothèses générées par éclatement d'une disjonction, ou 
-   des équations. Le constructeur terminal indique comment résoudre le système
-   obtenu en recourrant au type de trace d'Omega [t_omega] *)
+(* This type allows to extract useful components from hypothesis, either
+   hypothesis generated by splitting a disjonction, or equations. 
+   The last constructor indicates how to solve the obtained system 
+   via the use of the trace type of Omega [t_omega] *)
 
 Inductive e_step : Set :=
   | E_SPLIT : nat -> list direction -> e_step -> e_step -> e_step
   | E_EXTRACT : nat -> list direction -> e_step -> e_step
   | E_SOLVE : t_omega -> e_step.
 
-(* \subsection{Egalité décidable efficace} *)
-(* Pour chaque type de donnée réifié, on calcule un test d'égalité efficace.
-   Ce n'est pas le cas de celui rendu par [Decide Equality].
+(* \subsection{Efficient decidable equality} *)
+(* For each reified data-type, we define an efficient equality test. 
+   It is not the one produced by [Decide Equality].
    
-   Puis on prouve deux théorèmes permettant d'éliminer de telles égalités :
+   Then we prove two theorem allowing to eliminate such equalities : 
    \begin{verbatim}
    (t1,t2: typ) (eq_typ t1 t2) = true -> t1 = t2.
    (t1,t2: typ) (eq_typ t1 t2) = false -> ~ t1 = t2.
    \end{verbatim} *)
 
-(* Ces deux tactiques permettent de résoudre pas mal de cas. L'une pour
-   les théorèmes positifs, l'autre pour les théorèmes négatifs *)
-
-Ltac absurd_case := simpl in |- *; intros; discriminate.
-Ltac trivial_case := unfold not in |- *; intros; discriminate.
-
-(* \subsubsection{Entiers naturels} *)
-
-Fixpoint eq_nat (t1 t2 : nat) {struct t2} : bool :=
-  match t1 with
-  | O => match t2 with
-         | O => true
-         | _ => false
-         end
-  | S n1 => match t2 with
-            | O => false
-            | S n2 => eq_nat n1 n2
-            end
-  end.
-
-Theorem eq_nat_true : forall t1 t2 : nat, eq_nat t1 t2 = true -> t1 = t2.
-
-simple induction t1;
- [ intro t2; case t2; [ trivial | absurd_case ]
- | intros n H t2; case t2;
-    [ absurd_case
-    | simpl in |- *; intros; rewrite (H n0); [ trivial | assumption ] ] ].
-
-Qed.
-  
-Theorem eq_nat_false : forall t1 t2 : nat, eq_nat t1 t2 = false -> t1 <> t2.
-
-simple induction t1;
- [ intro t2; case t2; [ simpl in |- *; intros; discriminate | trivial_case ]
- | intros n H t2; case t2; simpl in |- *; unfold not in |- *; intros;
-    [ discriminate | elim (H n0 H0); simplify_eq H1; trivial ] ].
-
-Qed.
-                                   
-
-(* \subsubsection{Entiers positifs} *)
+(* \subsubsection{Reified terms} *)
 
-Fixpoint eq_pos (p1 p2 : positive) {struct p2} : bool :=
-  match p1 with
-  | xI n1 => match p2 with
-             | xI n2 => eq_pos n1 n2
-             | _ => false
-             end
-  | xO n1 => match p2 with
-             | xO n2 => eq_pos n1 n2
-             | _ => false
-             end
-  | xH => match p2 with
-          | xH => true
-          | _ => false
-          end
-  end.
+Open Scope romega_scope.
 
-Theorem eq_pos_true : forall t1 t2 : positive, eq_pos t1 t2 = true -> t1 = t2.
-
-simple induction t1;
- [ intros p H t2; case t2;
-    [ simpl in |- *; intros; rewrite (H p0 H0); trivial
-    | absurd_case
-    | absurd_case ]
- | intros p H t2; case t2;
-    [ absurd_case
-    | simpl in |- *; intros; rewrite (H p0 H0); trivial
-    | absurd_case ]
- | intro t2; case t2; [ absurd_case | absurd_case | auto ] ].
-
-Qed.
-  
-Theorem eq_pos_false :
- forall t1 t2 : positive, eq_pos t1 t2 = false -> t1 <> t2.
-
-simple induction t1;
- [ intros p H t2; case t2;
-    [ simpl in |- *; unfold not in |- *; intros; elim (H p0 H0);
-       simplify_eq H1; auto
-    | trivial_case
-    | trivial_case ]
- | intros p H t2; case t2;
-    [ trivial_case
-    | simpl in |- *; unfold not in |- *; intros; elim (H p0 H0);
-       simplify_eq H1; auto
-    | trivial_case ]
- | intros t2; case t2; [ trivial_case | trivial_case | absurd_case ] ].
-Qed.
-
-(* \subsubsection{Entiers relatifs} *)
-
-Definition eq_Z (z1 z2 : Z) : bool :=
-  match z1 with
-  | Z0 => match z2 with
-          | Z0 => true
-          | _ => false
-          end
-  | Zpos p1 => match z2 with
-               | Zpos p2 => eq_pos p1 p2
-               | _ => false
-               end
-  | Zneg p1 => match z2 with
-               | Zneg p2 => eq_pos p1 p2
-               | _ => false
-               end
+Fixpoint eq_term (t1 t2 : term) {struct t2} : bool :=
+  match t1, t2 with
+  | Tint st1, Tint st2 => beq st1 st2
+  | (st11 + st12), (st21 + st22) => eq_term st11 st21 && eq_term st12 st22
+  | (st11 * st12), (st21 * st22) => eq_term st11 st21 && eq_term st12 st22
+  | (st11 - st12), (st21 - st22) => eq_term st11 st21 && eq_term st12 st22
+  | (- st1), (- st2) => eq_term st1 st2
+  | [st1], [st2] => beq_nat st1 st2
+  | _, _ => false
   end.
 
-Theorem eq_Z_true : forall t1 t2 : Z, eq_Z t1 t2 = true -> t1 = t2.
-
-simple induction t1;
- [ intros t2; case t2; [ auto | absurd_case | absurd_case ]
- | intros p t2; case t2;
-    [ absurd_case
-    | simpl in |- *; intros; rewrite (eq_pos_true p p0 H); trivial
-    | absurd_case ]
- | intros p t2; case t2;
-    [ absurd_case
-    | absurd_case
-    | simpl in |- *; intros; rewrite (eq_pos_true p p0 H); trivial ] ].
-
-Qed.
-
-Theorem eq_Z_false : forall t1 t2 : Z, eq_Z t1 t2 = false -> t1 <> t2.
-
-simple induction t1;
- [ intros t2; case t2; [ absurd_case | trivial_case | trivial_case ]
- | intros p t2; case t2;
-    [ absurd_case
-    | simpl in |- *; unfold not in |- *; intros; elim (eq_pos_false p p0 H);
-       simplify_eq H0; auto
-    | trivial_case ]
- | intros p t2; case t2;
-    [ absurd_case
-    | trivial_case
-    | simpl in |- *; unfold not in |- *; intros; elim (eq_pos_false p p0 H);
-       simplify_eq H0; auto ] ].
-Qed.
-
-(* \subsubsection{Termes réifiés} *)
-
-Fixpoint eq_term (t1 t2 : term) {struct t2} : bool :=
-  match t1 with
-  | Tint st1 => match t2 with
-                | Tint st2 => eq_Z st1 st2
-                | _ => false
-                end
-  | (st11 + st12)%term =>
-      match t2 with
-      | (st21 + st22)%term => eq_term st11 st21 && eq_term st12 st22
-      | _ => false
-      end
-  | (st11 * st12)%term =>
-      match t2 with
-      | (st21 * st22)%term => eq_term st11 st21 && eq_term st12 st22
-      | _ => false
-      end
-  | (st11 - st12)%term =>
-      match t2 with
-      | (st21 - st22)%term => eq_term st11 st21 && eq_term st12 st22
-      | _ => false
-      end
-  | (- st1)%term =>
-      match t2 with
-      | (- st2)%term => eq_term st1 st2
-      | _ => false
-      end
-  | [st1]%term =>
-      match t2 with
-      | [st2]%term => eq_nat st1 st2
-      | _ => false
-      end
-  end.  
+Close Scope romega_scope.  
 
 Theorem eq_term_true : forall t1 t2 : term, eq_term t1 t2 = true -> t1 = t2.
-
-
-simple induction t1; intros until t2; case t2; try absurd_case; simpl in |- *;
- [ intros; elim eq_Z_true with (1 := H); trivial
+Proof.
+ simple induction t1; intros until t2; case t2; simpl in *;
+ try (intros; discriminate; fail); 
+ [ intros; elim beq_true with (1 := H); trivial
  | intros t21 t22 H3; elim andb_prop with (1 := H3); intros H4 H5;
     elim H with (1 := H4); elim H0 with (1 := H5); 
     trivial
@@ -417,16 +1074,17 @@ simple induction t1; intros until t2; case t2; try absurd_case; simpl in |- *;
     elim H with (1 := H4); elim H0 with (1 := H5); 
     trivial
  | intros t21 H3; elim H with (1 := H3); trivial
- | intros; elim eq_nat_true with (1 := H); trivial ].
-
+ | intros; elim beq_nat_true with (1 := H); trivial ].
 Qed.
 
+Ltac trivial_case := unfold not in |- *; intros; discriminate.
+
 Theorem eq_term_false :
  forall t1 t2 : term, eq_term t1 t2 = false -> t1 <> t2.
-
-simple induction t1;
+Proof.
+ simple induction t1;
  [ intros z t2; case t2; try trivial_case; simpl in |- *; unfold not in |- *;
-    intros; elim eq_Z_false with (1 := H); simplify_eq H0; 
+    intros; elim beq_false with (1 := H); simplify_eq H0; 
     auto
  | intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl in |- *;
     intros t21 t22 H3; unfold not in |- *; intro H4;
@@ -447,9 +1105,8 @@ simple induction t1;
     unfold not in |- *; intro H4; elim H1 with (1 := H3); 
     simplify_eq H4; auto
  | intros n t2; case t2; try trivial_case; simpl in |- *; unfold not in |- *;
-    intros; elim eq_nat_false with (1 := H); simplify_eq H0; 
+    intros; elim beq_nat_false with (1 := H); simplify_eq H0; 
     auto ].
-
 Qed.
 
 (* \subsubsection{Tactiques pour éliminer ces tests} 
@@ -463,54 +1120,29 @@ Qed.
    tel test préserve bien l'information voulue mais calculatoirement de
    telles fonctions sont trop lentes. *)
 
-(* Le théorème suivant permet de garder dans les hypothèses la valeur
-   du booléen lors de l'élimination. *)
-
-Theorem bool_ind2 :
- forall (P : bool -> Prop) (b : bool),
- (b = true -> P true) -> (b = false -> P false) -> P b.
-
-simple induction b; auto.
-Qed.
-
 (* Les tactiques définies si après se comportent exactement comme si on
    avait utilisé le test précédent et fait une elimination dessus. *)
 
 Ltac elim_eq_term t1 t2 :=
-  pattern (eq_term t1 t2) in |- *; apply bool_ind2; intro Aux;
+  pattern (eq_term t1 t2) in |- *; apply bool_eq_ind; intro Aux;
    [ generalize (eq_term_true t1 t2 Aux); clear Aux
    | generalize (eq_term_false t1 t2 Aux); clear Aux ].
 
-Ltac elim_eq_Z t1 t2 :=
-  pattern (eq_Z t1 t2) in |- *; apply bool_ind2; intro Aux;
-   [ generalize (eq_Z_true t1 t2 Aux); clear Aux
-   | generalize (eq_Z_false t1 t2 Aux); clear Aux ].
-
-Ltac elim_eq_pos t1 t2 :=
-  pattern (eq_pos t1 t2) in |- *; apply bool_ind2; intro Aux;
-   [ generalize (eq_pos_true t1 t2 Aux); clear Aux
-   | generalize (eq_pos_false t1 t2 Aux); clear Aux ].
+Ltac elim_beq t1 t2 :=
+  pattern (beq t1 t2) in |- *; apply bool_eq_ind; intro Aux;
+   [ generalize (beq_true t1 t2 Aux); clear Aux
+   | generalize (beq_false t1 t2 Aux); clear Aux ].
 
-(* \subsubsection{Comparaison sur Z} *)
-
-(* Sujet très lié au précédent : on introduit la tactique d'élimination
-   avec son théorème *)
-
-Theorem relation_ind2 :
- forall (P : comparison -> Prop) (b : comparison),
- (b = Eq -> P Eq) ->
- (b = Lt -> P Lt) ->
- (b = Gt -> P Gt) -> P b.
-
-simple induction b; auto.
-Qed.
+Ltac elim_bgt t1 t2 := 
+  pattern (bgt t1 t2) in |- *; apply bool_eq_ind; intro Aux; 
+  [ generalize (bgt_true t1 t2 Aux); clear Aux
+  | generalize (bgt_false t1 t2 Aux); clear Aux ].
 
-Ltac elim_Zcompare t1 t2 := pattern (t1 ?= t2) in |- *; apply relation_ind2.
 
 (* \subsection{Interprétations}
    \subsubsection{Interprétation des termes dans Z} *)
 
-Fixpoint interp_term (env : list Z) (t : term) {struct t} : Z :=
+Fixpoint interp_term (env : list int) (t : term) {struct t} : int :=
   match t with
   | Tint x => x
   | (t1 + t2)%term => interp_term env t1 + interp_term env t2
@@ -521,7 +1153,8 @@ Fixpoint interp_term (env : list Z) (t : term) {struct t} : Z :=
   end.
 
 (* \subsubsection{Interprétation des prédicats} *) 
-Fixpoint interp_proposition (envp : PropList) (env : list Z)
+
+Fixpoint interp_proposition (envp : list Prop) (env : list int)
  (p : proposition) {struct p} : Prop :=
   match p with
   | EqTerm t1 t2 => interp_term env t1 = interp_term env t2
@@ -532,14 +1165,14 @@ Fixpoint interp_proposition (envp : PropList) (env : list Z)
   | GeqTerm t1 t2 => interp_term env t1 >= interp_term env t2
   | GtTerm t1 t2 => interp_term env t1 > interp_term env t2
   | LtTerm t1 t2 => interp_term env t1 < interp_term env t2
-  | NeqTerm t1 t2 => Zne (interp_term env t1) (interp_term env t2)
+  | NeqTerm t1 t2 => (interp_term env t1)<>(interp_term env t2)
   | Tor p1 p2 =>
       interp_proposition envp env p1 \/ interp_proposition envp env p2
   | Tand p1 p2 =>
       interp_proposition envp env p1 /\ interp_proposition envp env p2
   | Timp p1 p2 =>
       interp_proposition envp env p1 -> interp_proposition envp env p2
-  | Tprop n => nthProp n envp True
+  | Tprop n => nth n envp True
   end.
 
 (* \subsubsection{Inteprétation des listes d'hypothèses}
@@ -547,7 +1180,7 @@ Fixpoint interp_proposition (envp : PropList) (env : list Z)
    Interprétation sous forme d'une conjonction d'hypothèses plus faciles
    à manipuler individuellement *)
 
-Fixpoint interp_hyps (envp : PropList) (env : list Z) 
+Fixpoint interp_hyps (envp : list Prop) (env : list int) 
  (l : hyps) {struct l} : Prop :=
   match l with
   | nil => True
@@ -559,8 +1192,8 @@ Fixpoint interp_hyps (envp : PropList) (env : list Z)
    [Generalize] et qu'une conjonction est forcément lourde (répétition des
    types dans les conjonctions intermédiaires) *)
 
-Fixpoint interp_goal_concl (c : proposition) (envp : PropList) 
- (env : list Z) (l : hyps) {struct l} : Prop :=
+Fixpoint interp_goal_concl (c : proposition) (envp : list Prop) 
+ (env : list int) (l : hyps) {struct l} : Prop :=
   match l with
   | nil => interp_proposition envp env c
   | p' :: l' =>
@@ -573,19 +1206,19 @@ Notation interp_goal := (interp_goal_concl FalseTerm).
    interprétations. *)
 
 Theorem goal_to_hyps :
- forall (envp : PropList) (env : list Z) (l : hyps),
+ forall (envp : list Prop) (env : list int) (l : hyps),
  (interp_hyps envp env l -> False) -> interp_goal envp env l.
-
-simple induction l;
+Proof.
+ simple induction l;
  [ simpl in |- *; auto
  | simpl in |- *; intros a l1 H1 H2 H3; apply H1; intro H4; apply H2; auto ].
 Qed.
 
 Theorem hyps_to_goal :
- forall (envp : PropList) (env : list Z) (l : hyps),
+ forall (envp : list Prop) (env : list int) (l : hyps),
  interp_goal envp env l -> interp_hyps envp env l -> False.
-
-simple induction l; simpl in |- *; [ auto | intros; apply H; elim H1; auto ].
+Proof.
+ simple induction l; simpl in |- *; [ auto | intros; apply H; elim H1; auto ].
 Qed.
       
 (* \subsection{Manipulations sur les hypothèses} *)
@@ -593,7 +1226,7 @@ Qed.
 (* \subsubsection{Définitions de base de stabilité pour la réflexion} *)
 (* Une opération laisse un terme stable si l'égalité est préservée *)
 Definition term_stable (f : term -> term) :=
-  forall (e : list Z) (t : term), interp_term e t = interp_term e (f t).
+  forall (e : list int) (t : term), interp_term e t = interp_term e (f t).
 
 (* Une opération est valide sur une hypothèse, si l'hypothèse implique le
    résultat de l'opération. \emph{Attention : cela ne concerne que des 
@@ -602,11 +1235,11 @@ Definition term_stable (f : term -> term) :=
    en argument (cela suffit pour omega). *)
 
 Definition valid1 (f : proposition -> proposition) :=
-  forall (ep : PropList) (e : list Z) (p1 : proposition),
+  forall (ep : list Prop) (e : list int) (p1 : proposition),
   interp_proposition ep e p1 -> interp_proposition ep e (f p1).
 
 Definition valid2 (f : proposition -> proposition -> proposition) :=
-  forall (ep : PropList) (e : list Z) (p1 p2 : proposition),
+  forall (ep : list Prop) (e : list int) (p1 p2 : proposition),
   interp_proposition ep e p1 ->
   interp_proposition ep e p2 -> interp_proposition ep e (f p1 p2).
 
@@ -615,31 +1248,31 @@ Definition valid2 (f : proposition -> proposition -> proposition) :=
    On reste contravariant *)
 
 Definition valid_hyps (f : hyps -> hyps) :=
-  forall (ep : PropList) (e : list Z) (lp : hyps),
+  forall (ep : list Prop) (e : list int) (lp : hyps),
   interp_hyps ep e lp -> interp_hyps ep e (f lp).
 
 (* Enfin ce théorème élimine la contravariance et nous ramène à une 
    opération sur les buts *)
 
- Theorem valid_goal :
-  forall (ep : PropList) (env : list Z) (l : hyps) (a : hyps -> hyps),
+Theorem valid_goal :
+  forall (ep : list Prop) (env : list int) (l : hyps) (a : hyps -> hyps),
   valid_hyps a -> interp_goal ep env (a l) -> interp_goal ep env l.
-
-intros; simpl in |- *; apply goal_to_hyps; intro H1;
+Proof.
+ intros; simpl in |- *; apply goal_to_hyps; intro H1;
  apply (hyps_to_goal ep env (a l) H0); apply H; assumption.
 Qed.
 
 (* \subsubsection{Généralisation a des listes de buts (disjonctions)} *)
 
 
-Fixpoint interp_list_hyps (envp : PropList) (env : list Z) 
+Fixpoint interp_list_hyps (envp : list Prop) (env : list int) 
  (l : lhyps) {struct l} : Prop :=
   match l with
   | nil => False
   | h :: l' => interp_hyps envp env h \/ interp_list_hyps envp env l'
   end.
 
-Fixpoint interp_list_goal (envp : PropList) (env : list Z) 
+Fixpoint interp_list_goal (envp : list Prop) (env : list int) 
  (l : lhyps) {struct l} : Prop :=
   match l with
   | nil => True
@@ -647,10 +1280,10 @@ Fixpoint interp_list_goal (envp : PropList) (env : list Z)
   end.
 
 Theorem list_goal_to_hyps :
- forall (envp : PropList) (env : list Z) (l : lhyps),
+ forall (envp : list Prop) (env : list int) (l : lhyps),
  (interp_list_hyps envp env l -> False) -> interp_list_goal envp env l.
-
-simple induction l; simpl in |- *;
+Proof.
+ simple induction l; simpl in |- *;
  [ auto
  | intros h1 l1 H H1; split;
     [ apply goal_to_hyps; intro H2; apply H1; auto
@@ -658,37 +1291,37 @@ simple induction l; simpl in |- *;
 Qed.
 
 Theorem list_hyps_to_goal :
- forall (envp : PropList) (env : list Z) (l : lhyps),
+ forall (envp : list Prop) (env : list int) (l : lhyps),
  interp_list_goal envp env l -> interp_list_hyps envp env l -> False.
-
-simple induction l; simpl in |- *;
+Proof.
+ simple induction l; simpl in |- *;
  [ auto
  | intros h1 l1 H (H1, H2) H3; elim H3; intro H4;
     [ apply hyps_to_goal with (1 := H1); assumption | auto ] ].
 Qed.
 
 Definition valid_list_hyps (f : hyps -> lhyps) :=
-  forall (ep : PropList) (e : list Z) (lp : hyps),
+  forall (ep : list Prop) (e : list int) (lp : hyps),
   interp_hyps ep e lp -> interp_list_hyps ep e (f lp).
 
 Definition valid_list_goal (f : hyps -> lhyps) :=
-  forall (ep : PropList) (e : list Z) (lp : hyps),
+  forall (ep : list Prop) (e : list int) (lp : hyps),
   interp_list_goal ep e (f lp) -> interp_goal ep e lp.
 
 Theorem goal_valid :
  forall f : hyps -> lhyps, valid_list_hyps f -> valid_list_goal f.
-
-unfold valid_list_goal in |- *; intros f H ep e lp H1; apply goal_to_hyps;
+Proof.
+ unfold valid_list_goal in |- *; intros f H ep e lp H1; apply goal_to_hyps;
  intro H2; apply list_hyps_to_goal with (1 := H1); 
  apply (H ep e lp); assumption.
 Qed.
  
 Theorem append_valid :
- forall (ep : PropList) (e : list Z) (l1 l2 : lhyps),
+ forall (ep : list Prop) (e : list int) (l1 l2 : lhyps),
  interp_list_hyps ep e l1 \/ interp_list_hyps ep e l2 ->
  interp_list_hyps ep e (l1 ++ l2).
-
-intros ep e; simple induction l1;
+Proof.
+ intros ep e; simple induction l1;
  [ simpl in |- *; intros l2 [H| H]; [ contradiction | trivial ]
  | simpl in |- *; intros h1 t1 HR l2 [[H| H]| H];
     [ auto
@@ -703,10 +1336,10 @@ Qed.
 Definition nth_hyps (n : nat) (l : hyps) := nth n l TrueTerm.
 
 Theorem nth_valid :
- forall (ep : PropList) (e : list Z) (i : nat) (l : hyps),
+ forall (ep : list Prop) (e : list int) (i : nat) (l : hyps),
  interp_hyps ep e l -> interp_proposition ep e (nth_hyps i l).
-
-unfold nth_hyps in |- *; simple induction i;
+Proof.
+ unfold nth_hyps in |- *; simple induction i;
  [ simple induction l; simpl in |- *; [ auto | intros; elim H0; auto ]
  | intros n H; simple induction l;
     [ simpl in |- *; trivial
@@ -722,8 +1355,8 @@ Definition apply_oper_2 (i j : nat)
 Theorem apply_oper_2_valid :
  forall (i j : nat) (f : proposition -> proposition -> proposition),
  valid2 f -> valid_hyps (apply_oper_2 i j f).
-
-intros i j f Hf; unfold apply_oper_2, valid_hyps in |- *; simpl in |- *;
+Proof.
+ intros i j f Hf; unfold apply_oper_2, valid_hyps in |- *; simpl in |- *;
  intros lp Hlp; split; [ apply Hf; apply nth_valid; assumption | assumption ].
 Qed.
 
@@ -743,8 +1376,8 @@ Fixpoint apply_oper_1 (i : nat) (f : proposition -> proposition)
 Theorem apply_oper_1_valid :
  forall (i : nat) (f : proposition -> proposition),
  valid1 f -> valid_hyps (apply_oper_1 i f).
-
-unfold valid_hyps in |- *; intros i f Hf ep e; elim i;
+Proof.
+ unfold valid_hyps in |- *; intros i f Hf ep e; elim i;
  [ intro lp; case lp;
     [ simpl in |- *; trivial
     | simpl in |- *; intros p l' (H1, H2); split;
@@ -753,7 +1386,6 @@ unfold valid_hyps in |- *; intros i f Hf ep e; elim i;
     [ simpl in |- *; auto
     | simpl in |- *; intros p l' (H1, H2); split;
        [ assumption | apply Hrec; assumption ] ] ].
-
 Qed.
 
 (* \subsubsection{Manipulations de termes} *)
@@ -789,31 +1421,31 @@ Definition apply_both (f g : term -> term) (t : term) :=
 
 Theorem apply_left_stable :
  forall f : term -> term, term_stable f -> term_stable (apply_left f).
-
-unfold term_stable in |- *; intros f H e t; case t; auto; simpl in |- *;
+Proof.
+ unfold term_stable in |- *; intros f H e t; case t; auto; simpl in |- *;
  intros; elim H; trivial.
 Qed.
 
 Theorem apply_right_stable :
  forall f : term -> term, term_stable f -> term_stable (apply_right f).
-
-unfold term_stable in |- *; intros f H e t; case t; auto; simpl in |- *;
+Proof.
+ unfold term_stable in |- *; intros f H e t; case t; auto; simpl in |- *;
  intros t0 t1; elim H; trivial.
 Qed.
 
 Theorem apply_both_stable :
  forall f g : term -> term,
  term_stable f -> term_stable g -> term_stable (apply_both f g).
-
-unfold term_stable in |- *; intros f g H1 H2 e t; case t; auto; simpl in |- *;
+Proof.
+ unfold term_stable in |- *; intros f g H1 H2 e t; case t; auto; simpl in |- *;
  intros t0 t1; elim H1; elim H2; trivial.
 Qed.
 
 Theorem compose_term_stable :
  forall f g : term -> term,
  term_stable f -> term_stable g -> term_stable (fun t : term => f (g t)).
-
-unfold term_stable in |- *; intros f g Hf Hg e t; elim Hf; apply Hg.
+Proof.
+ unfold term_stable in |- *; intros f g Hf Hg e t; elim Hf; apply Hg.
 Qed.
 
 (* \subsection{Les règles de réécriture} *)
@@ -879,21 +1511,7 @@ Ltac loop t :=
     | Tand x x0 => _
     | Timp x x0 => _
     | Tprop x => _
-    end =>
-       case X1;
-       [ intro; intro
-       | intro; intro
-       | idtac
-       | idtac
-       | intro
-       | intro; intro
-       | intro; intro
-       | intro; intro
-       | intro; intro
-       | intro; intro
-       | intro; intro
-       | intro; intro
-       | intro ]; auto; Simplify
+    end => destruct X1; auto; Simplify
   | match ?X1 with
     | Tint x => _
     | (x + x0)%term => _
@@ -901,38 +1519,27 @@ Ltac loop t :=
     | (x - x0)%term => _
     | (- x)%term => _
     | [x]%term => _
-    end =>
-      case X1;
-       [ intro | intro; intro | intro; intro | intro; intro | intro | intro ];
-       auto; Simplify
-  | match ?X1 ?= ?X2 with
-    | Eq => _
-    | Lt => _
-    | Gt => _
-    end =>
-      elim_Zcompare X1 X2; intro; auto; Simplify
-  | match ?X1 with
-    | Z0 => _
-    | Zpos x => _
-    | Zneg x => _
-    end =>
-      case X1; [ idtac | intro | intro ]; auto; Simplify
-  | (if eq_Z ?X1 ?X2 then _ else _) =>
-      elim_eq_Z X1 X2; intro H; [ rewrite H; clear H | clear H ];
+    end => destruct X1; auto; Simplify
+  | (if beq ?X1 ?X2 then _ else _) =>
+      let H := fresh "H" in 
+      elim_beq X1 X2; intro H; try (rewrite H in *; clear H);
        simpl in |- *; auto; Simplify
+  | (if bgt ?X1 ?X2 then _ else _) =>
+      let H := fresh "H" in 
+      elim_bgt X1 X2; intro H; simpl in |- *; auto; Simplify
   | (if eq_term ?X1 ?X2 then _ else _) =>
-      elim_eq_term X1 X2; intro H; [ rewrite H; clear H | clear H ];
-       simpl in |- *; auto; Simplify
-  | (if eq_pos ?X1 ?X2 then _ else _) =>
-      elim_eq_pos X1 X2; intro H; [ rewrite H; clear H | clear H ];
+      let H := fresh "H" in 
+      elim_eq_term X1 X2; intro H; try (rewrite H in *; clear H); 
        simpl in |- *; auto; Simplify
+  | (if _ && _ then _ else _) => rewrite andb_if; Simplify
+  | (if negb _ then _ else _) => rewrite negb_if; Simplify
   | _ => fail
   end
- with Simplify := match goal with
-                  |  |- ?X1 => try loop X1
-                  | _ => idtac
-                  end.
 
+with Simplify := match goal with
+  |  |- ?X1 => try loop X1
+  | _ => idtac
+  end.
 
 Ltac prove_stable x th :=
   match constr:x with
@@ -949,8 +1556,8 @@ Definition Tplus_assoc_l (t : term) :=
   end.
 
 Theorem Tplus_assoc_l_stable : term_stable Tplus_assoc_l.
-
-prove_stable Tplus_assoc_l Zplus_assoc.
+Proof.
+ prove_stable Tplus_assoc_l (ring.(Radd_assoc)).
 Qed.
 
 Definition Tplus_assoc_r (t : term) :=
@@ -960,8 +1567,8 @@ Definition Tplus_assoc_r (t : term) :=
   end.
 
 Theorem Tplus_assoc_r_stable : term_stable Tplus_assoc_r.
-
-prove_stable Tplus_assoc_r Zplus_assoc_reverse.
+Proof.
+ prove_stable Tplus_assoc_r plus_assoc_reverse.
 Qed.
 
 Definition Tmult_assoc_r (t : term) :=
@@ -971,8 +1578,8 @@ Definition Tmult_assoc_r (t : term) :=
   end.
 
 Theorem Tmult_assoc_r_stable : term_stable Tmult_assoc_r.
-
-prove_stable Tmult_assoc_r Zmult_assoc_reverse.
+Proof.
+ prove_stable Tmult_assoc_r mult_assoc_reverse.
 Qed.
 
 Definition Tplus_permute (t : term) :=
@@ -982,46 +1589,44 @@ Definition Tplus_permute (t : term) :=
   end.
 
 Theorem Tplus_permute_stable : term_stable Tplus_permute.
-
-prove_stable Tplus_permute Zplus_permute.
+Proof.
+ prove_stable Tplus_permute plus_permute.
 Qed.
 
-Definition Tplus_sym (t : term) :=
+Definition Tplus_comm (t : term) :=
   match t with
   | (x + y)%term => (y + x)%term
   | _ => t
   end.
 
-Theorem Tplus_sym_stable : term_stable Tplus_sym.
-
-prove_stable Tplus_sym Zplus_comm.
+Theorem Tplus_comm_stable : term_stable Tplus_comm.
+Proof.
+ prove_stable Tplus_comm plus_comm.
 Qed.
 
-Definition Tmult_sym (t : term) :=
+Definition Tmult_comm (t : term) :=
   match t with
   | (x * y)%term => (y * x)%term
   | _ => t
   end.
 
-Theorem Tmult_sym_stable : term_stable Tmult_sym.
-
-prove_stable Tmult_sym Zmult_comm.
+Theorem Tmult_comm_stable : term_stable Tmult_comm.
+Proof.
+ prove_stable Tmult_comm mult_comm.
 Qed.
 
 Definition T_OMEGA10 (t : term) :=
   match t with
   | ((v * Tint c1 + l1) * Tint k1 + (v' * Tint c2 + l2) * Tint k2)%term =>
-      match eq_term v v' with
-      | true =>
-          (v * Tint (c1 * k1 + c2 * k2) + (l1 * Tint k1 + l2 * Tint k2))%term
-      | false => t
-      end
+      if eq_term v v' 
+      then (v * Tint (c1 * k1 + c2 * k2)%I + (l1 * Tint k1 + l2 * Tint k2))%term
+      else t
   | _ => t
   end.
 
 Theorem T_OMEGA10_stable : term_stable T_OMEGA10.
-
-prove_stable T_OMEGA10 OMEGA10.
+Proof.
+ prove_stable T_OMEGA10 OMEGA10.
 Qed.
 
 Definition T_OMEGA11 (t : term) :=
@@ -1032,8 +1637,8 @@ Definition T_OMEGA11 (t : term) :=
   end.
 
 Theorem T_OMEGA11_stable : term_stable T_OMEGA11.
-
-prove_stable T_OMEGA11 OMEGA11.
+Proof.
+ prove_stable T_OMEGA11 OMEGA11.
 Qed.
 
 Definition T_OMEGA12 (t : term) :=
@@ -1044,52 +1649,37 @@ Definition T_OMEGA12 (t : term) :=
   end.
 
 Theorem T_OMEGA12_stable : term_stable T_OMEGA12.
-
-prove_stable T_OMEGA12 OMEGA12.
+Proof.
+ prove_stable T_OMEGA12 OMEGA12.
 Qed. 
 
 Definition T_OMEGA13 (t : term) :=
   match t with
-  | (v * Tint (Zpos x) + l1 + (v' * Tint (Zneg x') + l2))%term =>
-      match eq_term v v' with
-      | true =>
-          match eq_pos x x' with
-          | true => (l1 + l2)%term
-          | false => t
-          end
-      | false => t
-      end
-  | (v * Tint (Zneg x) + l1 + (v' * Tint (Zpos x') + l2))%term =>
-      match eq_term v v' with
-      | true =>
-          match eq_pos x x' with
-          | true => (l1 + l2)%term
-          | false => t
-          end
-      | false => t
-      end
+  | (v * Tint x + l1 + (v' * Tint x' + l2))%term =>
+      if eq_term v v' && beq x (-x') 
+      then (l1+l2)%term
+      else t
   | _ => t
   end.
 
 Theorem T_OMEGA13_stable : term_stable T_OMEGA13.
-
-unfold term_stable, T_OMEGA13 in |- *; intros; Simplify; simpl in |- *;
- [ apply OMEGA13 | apply OMEGA14 ].
+Proof.
+ unfold term_stable, T_OMEGA13 in |- *; intros; Simplify; simpl in |- *;
+ apply OMEGA13.
 Qed.
 
 Definition T_OMEGA15 (t : term) :=
   match t with
   | (v * Tint c1 + l1 + (v' * Tint c2 + l2) * Tint k2)%term =>
-      match eq_term v v' with
-      | true => (v * Tint (c1 + c2 * k2) + (l1 + l2 * Tint k2))%term
-      | false => t
-      end
+      if eq_term v v' 
+      then (v * Tint (c1 + c2 * k2)%I + (l1 + l2 * Tint k2))%term
+      else t
   | _ => t
   end.
 
 Theorem T_OMEGA15_stable : term_stable T_OMEGA15.
-
-prove_stable T_OMEGA15 OMEGA15.
+Proof.
+ prove_stable T_OMEGA15 OMEGA15.
 Qed.
 
 Definition T_OMEGA16 (t : term) :=
@@ -1100,20 +1690,19 @@ Definition T_OMEGA16 (t : term) :=
 
 
 Theorem T_OMEGA16_stable : term_stable T_OMEGA16.
-
-prove_stable T_OMEGA16 OMEGA16.
+Proof.
+ prove_stable T_OMEGA16 OMEGA16.
 Qed.
 
 Definition Tred_factor5 (t : term) :=
   match t with
-  | (x * Tint Z0 + y)%term => y
+  | (x * Tint c + y)%term => if beq c 0 then y else t
   | _ => t
   end.
 
 Theorem Tred_factor5_stable : term_stable Tred_factor5.
-
-
-prove_stable Tred_factor5 Zred_factor5.
+Proof.
+ prove_stable Tred_factor5 red_factor5.
 Qed.
 
 Definition Topp_plus (t : term) :=
@@ -1123,8 +1712,8 @@ Definition Topp_plus (t : term) :=
   end.
 
 Theorem Topp_plus_stable : term_stable Topp_plus.
-
-prove_stable Topp_plus Zopp_plus_distr.
+Proof.
+ prove_stable Topp_plus opp_plus_distr.
 Qed.
 
 
@@ -1135,8 +1724,8 @@ Definition Topp_opp (t : term) :=
   end.
 
 Theorem Topp_opp_stable : term_stable Topp_opp.
-
-prove_stable Topp_opp Zopp_involutive.
+Proof.
+ prove_stable Topp_opp opp_involutive.
 Qed.
 
 Definition Topp_mult_r (t : term) :=
@@ -1146,19 +1735,19 @@ Definition Topp_mult_r (t : term) :=
   end.
 
 Theorem Topp_mult_r_stable : term_stable Topp_mult_r.
-
-prove_stable Topp_mult_r Zopp_mult_distr_r.
+Proof.
+ prove_stable Topp_mult_r opp_mult_distr_r.
 Qed.
 
 Definition Topp_one (t : term) :=
   match t with
-  | (- x)%term => (x * Tint (-1))%term
+  | (- x)%term => (x * Tint (-(1)))%term
   | _ => t
   end.
 
 Theorem Topp_one_stable : term_stable Topp_one.
-
-prove_stable Topp_one Zopp_eq_mult_neg_1.
+Proof.
+ prove_stable Topp_one opp_eq_mult_neg_1.
 Qed.
 
 Definition Tmult_plus_distr (t : term) :=
@@ -1168,8 +1757,8 @@ Definition Tmult_plus_distr (t : term) :=
   end.
 
 Theorem Tmult_plus_distr_stable : term_stable Tmult_plus_distr.
-
-prove_stable Tmult_plus_distr Zmult_plus_distr_l.
+Proof.
+ prove_stable Tmult_plus_distr mult_plus_distr_r.
 Qed.
 
 Definition Tmult_opp_left (t : term) :=
@@ -1179,8 +1768,8 @@ Definition Tmult_opp_left (t : term) :=
   end.
 
 Theorem Tmult_opp_left_stable : term_stable Tmult_opp_left.
-
-prove_stable Tmult_opp_left Zmult_opp_comm.
+Proof.
+ prove_stable Tmult_opp_left mult_opp_comm.
 Qed.
 
 Definition Tmult_assoc_reduced (t : term) :=
@@ -1190,91 +1779,81 @@ Definition Tmult_assoc_reduced (t : term) :=
   end.
 
 Theorem Tmult_assoc_reduced_stable : term_stable Tmult_assoc_reduced.
-
-prove_stable Tmult_assoc_reduced Zmult_assoc_reverse.
+Proof.
+ prove_stable Tmult_assoc_reduced mult_assoc_reverse.
 Qed.
 
 Definition Tred_factor0 (t : term) := (t * Tint 1)%term.
 
 Theorem Tred_factor0_stable : term_stable Tred_factor0.
-
-prove_stable Tred_factor0 Zred_factor0.
+Proof.
+ prove_stable Tred_factor0 red_factor0.
 Qed.
 
 Definition Tred_factor1 (t : term) :=
   match t with
   | (x + y)%term =>
-      match eq_term x y with
-      | true => (x * Tint 2)%term
-      | false => t
-      end
+      if eq_term x y 
+      then (x * Tint 2)%term
+      else t 
   | _ => t
   end.
 
 Theorem Tred_factor1_stable : term_stable Tred_factor1.
-
-prove_stable Tred_factor1 Zred_factor1.
+Proof.
+ prove_stable Tred_factor1 red_factor1.
 Qed.
 
 Definition Tred_factor2 (t : term) :=
   match t with
   | (x + y * Tint k)%term =>
-      match eq_term x y with
-      | true => (x * Tint (1 + k))%term
-      | false => t
-      end
+      if eq_term x y 
+      then (x * Tint (1 + k))%term
+      else t
   | _ => t
   end.
 
-(* Attention : il faut rendre opaque [Zplus] pour éviter que la tactique
-   de simplification n'aille trop loin et défasse [Zplus 1 k] *)
-
-Opaque Zplus.
-
 Theorem Tred_factor2_stable : term_stable Tred_factor2.
-prove_stable Tred_factor2 Zred_factor2.
+Proof.
+ prove_stable Tred_factor2 red_factor2.
 Qed.
 
 Definition Tred_factor3 (t : term) :=
   match t with
   | (x * Tint k + y)%term =>
-      match eq_term x y with
-      | true => (x * Tint (1 + k))%term
-      | false => t
-      end
+      if eq_term x y 
+      then (x * Tint (1 + k))%term
+      else t
   | _ => t
   end.
 
 Theorem Tred_factor3_stable : term_stable Tred_factor3.
-
-prove_stable Tred_factor3 Zred_factor3.
+Proof.
+ prove_stable Tred_factor3 red_factor3.
 Qed.
 
 
 Definition Tred_factor4 (t : term) :=
   match t with
   | (x * Tint k1 + y * Tint k2)%term =>
-      match eq_term x y with
-      | true => (x * Tint (k1 + k2))%term
-      | false => t
-      end
+      if eq_term x y 
+      then (x * Tint (k1 + k2))%term
+      else t
   | _ => t
   end.
 
 Theorem Tred_factor4_stable : term_stable Tred_factor4.
-
-prove_stable Tred_factor4 Zred_factor4.
+Proof.
+ prove_stable Tred_factor4 red_factor4.
 Qed.
 
 Definition Tred_factor6 (t : term) := (t + Tint 0)%term.
 
 Theorem Tred_factor6_stable : term_stable Tred_factor6.
-
-prove_stable Tred_factor6 Zred_factor6.
+Proof.
+ prove_stable Tred_factor6 red_factor6.
 Qed.
 
-Transparent Zplus.
-
 Definition Tminus_def (t : term) :=
   match t with
   | (x - y)%term => (x + - y)%term
@@ -1282,9 +1861,8 @@ Definition Tminus_def (t : term) :=
   end.
 
 Theorem Tminus_def_stable : term_stable Tminus_def.
-
-(* Le théorème ne sert à rien. Le but est prouvé avant. *)
-prove_stable Tminus_def False.
+Proof.
+ prove_stable Tminus_def minus_def.
 Qed.
 
 (* \subsection{Fonctions de réécriture complexes} *)
@@ -1332,8 +1910,8 @@ Fixpoint reduce (t : term) : term :=
   end.
 
 Theorem reduce_stable : term_stable reduce.
-
-unfold term_stable in |- *; intros e t; elim t; auto;
+Proof.
+ unfold term_stable in |- *; intros e t; elim t; auto;
  try
   (intros t0 H0 t1 H1; simpl in |- *; rewrite H0; rewrite H1;
     (case (reduce t0);
@@ -1366,8 +1944,8 @@ Fixpoint fusion (trace : list t_fusion) (t : term) {struct trace} : term :=
   end.
     
 Theorem fusion_stable : forall t : list t_fusion, term_stable (fusion t).
-
-simple induction t; simpl in |- *;
+Proof.
+ simple induction t; simpl in |- *;
  [ exact reduce_stable
  | intros stp l H; case stp;
     [ apply compose_term_stable;
@@ -1378,7 +1956,6 @@ simple induction t; simpl in |- *;
        [ apply apply_right_stable; assumption | exact T_OMEGA11_stable ]
     | apply compose_term_stable;
        [ apply apply_right_stable; assumption | exact T_OMEGA12_stable ] ] ].
-
 Qed.
 
 (* \paragraph{Fusion de deux équations dont une sans coefficient} *)
@@ -1405,8 +1982,8 @@ Fixpoint fusion_cancel (trace : nat) (t : term) {struct trace} : term :=
   end.
 
 Theorem fusion_cancel_stable : forall t : nat, term_stable (fusion_cancel t).
-
-unfold term_stable, fusion_cancel in |- *; intros trace e; elim trace;
+Proof.
+ unfold term_stable, fusion_cancel in |- *; intros trace e; elim trace;
  [ exact (reduce_stable e)
  | intros n H t; elim H; exact (T_OMEGA13_stable e t) ].
 Qed. 
@@ -1422,8 +1999,8 @@ Fixpoint scalar_norm_add (trace : nat) (t : term) {struct trace} : term :=
 
 Theorem scalar_norm_add_stable :
  forall t : nat, term_stable (scalar_norm_add t).
-
-unfold term_stable, scalar_norm_add in |- *; intros trace; elim trace;
+Proof.
+ unfold term_stable, scalar_norm_add in |- *; intros trace; elim trace;
  [ exact reduce_stable
  | intros n H e t; elim apply_right_stable;
     [ exact (T_OMEGA11_stable e t) | exact H ] ].
@@ -1437,8 +2014,8 @@ Fixpoint scalar_norm (trace : nat) (t : term) {struct trace} : term :=
   end.
 
 Theorem scalar_norm_stable : forall t : nat, term_stable (scalar_norm t).
-
-unfold term_stable, scalar_norm in |- *; intros trace; elim trace;
+Proof.
+ unfold term_stable, scalar_norm in |- *; intros trace; elim trace;
  [ exact reduce_stable
  | intros n H e t; elim apply_right_stable;
     [ exact (T_OMEGA16_stable e t) | exact H ] ].
@@ -1452,8 +2029,8 @@ Fixpoint add_norm (trace : nat) (t : term) {struct trace} : term :=
   end.
 
 Theorem add_norm_stable : forall t : nat, term_stable (add_norm t).
-
-unfold term_stable, add_norm in |- *; intros trace; elim trace;
+Proof.
+ unfold term_stable, add_norm in |- *; intros trace; elim trace;
  [ exact reduce_stable
  | intros n H e t; elim apply_right_stable;
     [ exact (Tplus_assoc_r_stable e t) | exact H ] ].
@@ -1480,7 +2057,7 @@ Fixpoint rewrite (s : step) : term -> term :=
   | C_PLUS_ASSOC_R => Tplus_assoc_r
   | C_PLUS_ASSOC_L => Tplus_assoc_l
   | C_PLUS_PERMUTE => Tplus_permute
-  | C_PLUS_COMM => Tplus_sym
+  | C_PLUS_COMM => Tplus_comm
   | C_RED0 => Tred_factor0
   | C_RED1 => Tred_factor1
   | C_RED2 => Tred_factor2
@@ -1490,12 +2067,12 @@ Fixpoint rewrite (s : step) : term -> term :=
   | C_RED6 => Tred_factor6
   | C_MULT_ASSOC_REDUCED => Tmult_assoc_reduced
   | C_MINUS => Tminus_def
-  | C_MULT_COMM => Tmult_sym
+  | C_MULT_COMM => Tmult_comm
   end.
 
 Theorem rewrite_stable : forall s : step, term_stable (rewrite s).
-
-simple induction s; simpl in |- *;
+Proof.
+ simple induction s; simpl in |- *;
  [ intros; apply apply_both_stable; auto
  | intros; apply apply_left_stable; auto
  | intros; apply apply_right_stable; auto
@@ -1512,7 +2089,7 @@ simple induction s; simpl in |- *;
  | exact Tplus_assoc_r_stable
  | exact Tplus_assoc_l_stable
  | exact Tplus_permute_stable
- | exact Tplus_sym_stable
+ | exact Tplus_comm_stable
  | exact Tred_factor0_stable
  | exact Tred_factor1_stable
  | exact Tred_factor2_stable
@@ -1522,7 +2099,7 @@ simple induction s; simpl in |- *;
  | exact Tred_factor6_stable
  | exact Tmult_assoc_reduced_stable
  | exact Tminus_def_stable
- | exact Tmult_sym_stable ].
+ | exact Tmult_comm_stable ].
 Qed.
 
 (* \subsection{tactiques de résolution d'un but omega normalisé} 
@@ -1532,20 +2109,18 @@ Qed.
 
 Definition constant_not_nul (i : nat) (h : hyps) :=
   match nth_hyps i h with
-  | EqTerm (Tint Z0) (Tint n) =>
-      match eq_Z n 0 with
-      | true => h
-      | false => absurd
-      end
+  | EqTerm (Tint Nul) (Tint n) =>
+      if beq n Nul then h else absurd
   | _ => h
   end.
 
 Theorem constant_not_nul_valid :
  forall i : nat, valid_hyps (constant_not_nul i).
-
-unfold valid_hyps, constant_not_nul in |- *; intros;
- generalize (nth_valid ep e i lp); Simplify; simpl in |- *;
- elim_eq_Z ipattern:z0 0; auto; simpl in |- *; intros H1 H2; 
+Proof.
+ unfold valid_hyps, constant_not_nul in |- *; intros;
+ generalize (nth_valid ep e i lp); Simplify; simpl in |- *. 
+ 
+ elim_beq i1 i0; auto; simpl in |- *; intros H1 H2; 
  elim H1; symmetry  in |- *; auto.
 Qed.   
 
@@ -1553,66 +2128,55 @@ Qed.
 
 Definition constant_neg (i : nat) (h : hyps) :=
   match nth_hyps i h with
-  | LeqTerm (Tint Z0) (Tint (Zneg n)) => absurd
+  | LeqTerm (Tint Nul) (Tint Neg) => 
+     if bgt Nul Neg then absurd else h
   | _ => h
   end.
 
 Theorem constant_neg_valid : forall i : nat, valid_hyps (constant_neg i).
-
-unfold valid_hyps, constant_neg in |- *; intros;
- generalize (nth_valid ep e i lp); Simplify; simpl in |- *;
- unfold Zle in |- *; simpl in |- *; intros H1; elim H1;
- [ assumption | trivial ].
-Qed.   
+Proof.
+ unfold valid_hyps, constant_neg in |- *; intros;
+ generalize (nth_valid ep e i lp); Simplify; simpl in |- *.
+ rewrite gt_lt_iff in H0; rewrite le_lt_iff; intuition.
+Qed.
 
 (* \paragraph{[NOT_EXACT_DIVIDE]} *)
-Definition not_exact_divide (k1 k2 : Z) (body : term) 
+Definition not_exact_divide (k1 k2 : int) (body : term) 
   (t i : nat) (l : hyps) :=
   match nth_hyps i l with
-  | EqTerm (Tint Z0) b =>
-      match
-        eq_term (scalar_norm_add t (body * Tint k1 + Tint k2)%term) b
-      with
-      | true =>
-          match k2 ?= 0 with
-          | Gt =>
-              match k1 ?= k2 with
-              | Gt => absurd
-              | _ => l
-              end
-          | _ => l
-          end
-      | false => l
-      end
+  | EqTerm (Tint Nul) b =>
+      if beq Nul 0 && 
+         eq_term (scalar_norm_add t (body * Tint k1 + Tint k2)%term) b && 
+         bgt k2 0 && 
+         bgt k1 k2 
+      then absurd
+      else l
   | _ => l
   end.
 
 Theorem not_exact_divide_valid :
- forall (k1 k2 : Z) (body : term) (t i : nat),
+ forall (k1 k2 : int) (body : term) (t i : nat),
  valid_hyps (not_exact_divide k1 k2 body t i).
-
-unfold valid_hyps, not_exact_divide in |- *; intros;
- generalize (nth_valid ep e i lp); Simplify;
- elim_eq_term (scalar_norm_add t (body * Tint k1 + Tint k2)%term) t1; 
- auto; Simplify; intro H2; elim H2; simpl in |- *;
- elim (scalar_norm_add_stable t e); simpl in |- *; 
- intro H4; absurd (interp_term e body * k1 + k2 = 0);
- [ apply OMEGA4; assumption | symmetry  in |- *; auto ].
-
+Proof.
+ unfold valid_hyps, not_exact_divide in |- *; intros;
+ generalize (nth_valid ep e i lp); Simplify.
+ rewrite (scalar_norm_add_stable t e), <-H1.
+ do 2 rewrite <- scalar_norm_add_stable; simpl in *; intros.
+ absurd (interp_term e body * k1 + k2 = 0); 
+ [ now apply OMEGA4 | symmetry; auto ].
 Qed.
 
 (* \paragraph{[O_CONTRADICTION]} *)
 
 Definition contradiction (t i j : nat) (l : hyps) :=
   match nth_hyps i l with
-  | LeqTerm (Tint Z0) b1 =>
+  | LeqTerm (Tint Nul) b1 =>
       match nth_hyps j l with
-      | LeqTerm (Tint Z0) b2 =>
+      | LeqTerm (Tint Nul') b2 =>
           match fusion_cancel t (b1 + b2)%term with
-          | Tint k => match 0 ?= k with
-                      | Gt => absurd
-                      | _ => l
-                      end
+          | Tint k => if beq Nul 0 && beq Nul' 0 && bgt 0 k 
+                      then absurd 
+                      else l
           | _ => l
           end
       | _ => l
@@ -1622,43 +2186,40 @@ Definition contradiction (t i j : nat) (l : hyps) :=
 
 Theorem contradiction_valid :
  forall t i j : nat, valid_hyps (contradiction t i j).
-
-unfold valid_hyps, contradiction in |- *; intros t i j ep e l H;
+Proof.
+ unfold valid_hyps, contradiction in |- *; intros t i j ep e l H;
  generalize (nth_valid _ _ i _ H); generalize (nth_valid _ _ j _ H);
  case (nth_hyps i l); auto; intros t1 t2; case t1; 
- auto; intros z; case z; auto; case (nth_hyps j l); 
- auto; intros t3 t4; case t3; auto; intros z'; case z'; 
- auto; simpl in |- *; intros H1 H2;
+ auto; case (nth_hyps j l); 
+ auto; intros t3 t4; case t3; auto; 
+ simpl in |- *; intros z z' H1 H2;
  generalize (refl_equal (interp_term e (fusion_cancel t (t2 + t4)%term)));
  pattern (fusion_cancel t (t2 + t4)%term) at 2 3 in |- *;
  case (fusion_cancel t (t2 + t4)%term); simpl in |- *; 
- auto; intro k; elim (fusion_cancel_stable t); simpl in |- *; 
- intro E; generalize (OMEGA2 _ _ H2 H1); rewrite E; 
- case k; auto; unfold Zle in |- *; simpl in |- *; intros p H3; 
- elim H3; auto.
-
+ auto; intro k; elim (fusion_cancel_stable t); simpl in |- *.
+ Simplify; intro H3.
+ generalize (OMEGA2 _ _ H2 H1); rewrite H3. 
+ rewrite gt_lt_iff in H0; rewrite le_lt_iff; intuition.
 Qed.
 
 (* \paragraph{[O_NEGATE_CONTRADICT]} *)
 
 Definition negate_contradict (i1 i2 : nat) (h : hyps) :=
   match nth_hyps i1 h with
-  | EqTerm (Tint Z0) b1 =>
+  | EqTerm (Tint Nul) b1 =>
       match nth_hyps i2 h with
-      | NeqTerm (Tint Z0) b2 =>
-          match eq_term b1 b2 with
-          | true => absurd
-          | false => h
-          end
+      | NeqTerm (Tint Nul') b2 =>
+          if beq Nul 0 && beq Nul' 0 && eq_term b1 b2 
+          then absurd 
+          else h
       | _ => h
       end
-  | NeqTerm (Tint Z0) b1 =>
+  | NeqTerm (Tint Nul) b1 =>
       match nth_hyps i2 h with
-      | EqTerm (Tint Z0) b2 =>
-          match eq_term b1 b2 with
-          | true => absurd
-          | false => h
-          end
+      | EqTerm (Tint Nul') b2 =>
+          if beq Nul 0 && beq Nul' 0 && eq_term b1 b2 
+          then absurd 
+          else h 
       | _ => h
       end
   | _ => h
@@ -1666,22 +2227,22 @@ Definition negate_contradict (i1 i2 : nat) (h : hyps) :=
 
 Definition negate_contradict_inv (t i1 i2 : nat) (h : hyps) :=
   match nth_hyps i1 h with
-  | EqTerm (Tint Z0) b1 =>
+  | EqTerm (Tint Nul) b1 =>
       match nth_hyps i2 h with
-      | NeqTerm (Tint Z0) b2 =>
-          match eq_term b1 (scalar_norm t (b2 * Tint (-1))%term) with
-          | true => absurd
-          | false => h
-          end
+      | NeqTerm (Tint Nul') b2 =>
+          if beq Nul 0 && beq Nul' 0 && 
+             eq_term b1 (scalar_norm t (b2 * Tint (-(1)))%term)
+          then absurd
+          else h
       | _ => h
       end
-  | NeqTerm (Tint Z0) b1 =>
+  | NeqTerm (Tint Nul) b1 =>
       match nth_hyps i2 h with
-      | EqTerm (Tint Z0) b2 =>
-          match eq_term b1 (scalar_norm t (b2 * Tint (-1))%term) with
-          | true => absurd
-          | false => h
-          end
+      | EqTerm (Tint Nul') b2 =>
+          if beq Nul 0 && beq Nul' 0 && 
+             eq_term b1 (scalar_norm t (b2 * Tint (-(1)))%term)
+          then absurd
+          else h
       | _ => h
       end
   | _ => h
@@ -1689,45 +2250,33 @@ Definition negate_contradict_inv (t i1 i2 : nat) (h : hyps) :=
 
 Theorem negate_contradict_valid :
  forall i j : nat, valid_hyps (negate_contradict i j).
-
-unfold valid_hyps, negate_contradict in |- *; intros i j ep e l H;
+Proof.
+ unfold valid_hyps, negate_contradict in |- *; intros i j ep e l H;
  generalize (nth_valid _ _ i _ H); generalize (nth_valid _ _ j _ H);
  case (nth_hyps i l); auto; intros t1 t2; case t1; 
- auto; intros z; case z; auto; case (nth_hyps j l); 
- auto; intros t3 t4; case t3; auto; intros z'; case z'; 
- auto; simpl in |- *; intros H1 H2;
- [ elim_eq_term t2 t4; intro H3;
-    [ elim H1; elim H3; assumption | assumption ]
- | elim_eq_term t2 t4; intro H3;
-    [ elim H2; rewrite H3; assumption | assumption ] ].
-
+ auto; intros z; auto; case (nth_hyps j l); 
+ auto; intros t3 t4; case t3; auto; intros z'; 
+ auto; simpl in |- *; intros H1 H2; Simplify.
 Qed.
 
 Theorem negate_contradict_inv_valid :
  forall t i j : nat, valid_hyps (negate_contradict_inv t i j).
-
-
-unfold valid_hyps, negate_contradict_inv in |- *; intros t i j ep e l H;
+Proof.
+ unfold valid_hyps, negate_contradict_inv in |- *; intros t i j ep e l H;
  generalize (nth_valid _ _ i _ H); generalize (nth_valid _ _ j _ H);
  case (nth_hyps i l); auto; intros t1 t2; case t1; 
- auto; intros z; case z; auto; case (nth_hyps j l); 
- auto; intros t3 t4; case t3; auto; intros z'; case z'; 
- auto; simpl in |- *; intros H1 H2;
- (pattern (eq_term t2 (scalar_norm t (t4 * Tint (-1))%term)) in |- *;
-   apply bool_ind2; intro Aux;
-   [ generalize (eq_term_true t2 (scalar_norm t (t4 * Tint (-1))%term) Aux);
-      clear Aux
-   | generalize (eq_term_false t2 (scalar_norm t (t4 * Tint (-1))%term) Aux);
-      clear Aux ]);
- [ intro H3; elim H1; generalize H2; rewrite H3;
-    rewrite <- (scalar_norm_stable t e); simpl in |- *;
-    elim (interp_term e t4); simpl in |- *; auto; intros p H4;
-    discriminate H4
- | auto
- | intro H3; elim H2; rewrite H3; elim (scalar_norm_stable t e);
-    simpl in |- *; elim H1; simpl in |- *; trivial
- | auto ].
-
+ auto; intros z; auto; case (nth_hyps j l); 
+ auto; intros t3 t4; case t3; auto; intros z'; 
+ auto; simpl in |- *; intros H1 H2; Simplify; 
+ [
+ rewrite <- scalar_norm_stable in H2; simpl in *;
+ elim (mult_integral (interp_term e t4) (-(1))); intuition;
+ elim minus_one_neq_zero; auto
+ | 
+ elim H2; clear H2;
+ rewrite <- scalar_norm_stable; simpl in *;
+ now rewrite <- H1, mult_0_l
+ ].
 Qed.
 
 (* \subsubsection{Tactiques générant une nouvelle équation} *)
@@ -1737,150 +2286,93 @@ Qed.
  preuve un peu compliquée. On utilise quelques lemmes qui sont des 
  généralisations des théorèmes utilisés par OMEGA. *)
 
-Definition sum (k1 k2 : Z) (trace : list t_fusion)
+Definition sum (k1 k2 : int) (trace : list t_fusion)
   (prop1 prop2 : proposition) :=
   match prop1 with
-  | EqTerm (Tint Z0) b1 =>
+  | EqTerm (Tint Null) b1 =>
       match prop2 with
-      | EqTerm (Tint Z0) b2 =>
-          EqTerm (Tint 0) (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term)
-      | LeqTerm (Tint Z0) b2 =>
-          match k2 ?= 0 with
-          | Gt =>
-              LeqTerm (Tint 0)
+      | EqTerm (Tint Null') b2 =>
+          if beq Null 0 && beq Null' 0 
+          then EqTerm (Tint 0) (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term)
+          else TrueTerm
+      | LeqTerm (Tint Null') b2 =>
+          if beq Null 0 && beq Null' 0 && bgt k2 0 
+          then LeqTerm (Tint 0)
                 (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term)
-          | _ => TrueTerm
-          end
+          else TrueTerm
       | _ => TrueTerm
       end
-  | LeqTerm (Tint Z0) b1 =>
-      match k1 ?= 0 with
-      | Gt =>
-          match prop2 with
-          | EqTerm (Tint Z0) b2 =>
+  | LeqTerm (Tint Null) b1 =>
+      if beq Null 0 && bgt k1 0
+      then match prop2 with
+          | EqTerm (Tint Null') b2 =>
+              if beq Null' 0 then 
               LeqTerm (Tint 0)
                 (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term)
-          | LeqTerm (Tint Z0) b2 =>
-              match k2 ?= 0 with
-              | Gt =>
-                  LeqTerm (Tint 0)
+              else TrueTerm  
+          | LeqTerm (Tint Null') b2 =>
+              if beq Null' 0 && bgt k2 0 
+              then LeqTerm (Tint 0)
                     (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term)
-              | _ => TrueTerm
-              end
+              else TrueTerm
           | _ => TrueTerm
           end
-      | _ => TrueTerm
-      end
-  | NeqTerm (Tint Z0) b1 =>
+      else TrueTerm 
+  | NeqTerm (Tint Null) b1 =>
       match prop2 with
-      | EqTerm (Tint Z0) b2 =>
-          match eq_Z k1 0 with
-          | true => TrueTerm
-          | false =>
-              NeqTerm (Tint 0)
-                (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term)
-          end
+      | EqTerm (Tint Null') b2 =>
+          if beq Null 0 && beq Null' 0 && (negb (beq k1 0))
+          then NeqTerm (Tint 0)
+                 (fusion trace (b1 * Tint k1 + b2 * Tint k2)%term)
+          else TrueTerm
       | _ => TrueTerm
       end
   | _ => TrueTerm
   end.
 
-Theorem sum1 : forall a b c d : Z, 0 = a -> 0 = b -> 0 = a * c + b * d.
-
-intros; elim H; elim H0; simpl in |- *; auto.
-Qed.
-  
-Theorem sum2 :
- forall a b c d : Z, 0 <= d -> 0 = a -> 0 <= b -> 0 <= a * c + b * d.
-
-intros; elim H0; simpl in |- *; generalize H H1; case b; case d;
- unfold Zle in |- *; simpl in |- *; auto.  
-Qed.
-
-Theorem sum3 :
- forall a b c d : Z,
- 0 <= c -> 0 <= d -> 0 <= a -> 0 <= b -> 0 <= a * c + b * d.
-
-intros a b c d; case a; case b; case c; case d; unfold Zle in |- *;
- simpl in |- *; auto. 
-Qed.
-
-Theorem sum4 : forall k : Z, (k ?= 0) = Gt -> 0 <= k.
-
-intro; case k; unfold Zle in |- *; simpl in |- *; auto; intros; discriminate.  
-Qed.
-
-Theorem sum5 :
- forall a b c d : Z, c <> 0 -> 0 <> a -> 0 = b -> 0 <> a * c + b * d.
-
-intros a b c d H1 H2 H3; elim H3; simpl in |- *; rewrite Zplus_comm;
- simpl in |- *; generalize H1 H2; case a; case c; simpl in |- *; 
- intros; try discriminate; assumption.
-Qed.
-
 
 Theorem sum_valid :
- forall (k1 k2 : Z) (t : list t_fusion), valid2 (sum k1 k2 t).
-
-unfold valid2 in |- *; intros k1 k2 t ep e p1 p2; unfold sum in |- *;
+ forall (k1 k2 : int) (t : list t_fusion), valid2 (sum k1 k2 t).
+Proof.
+ unfold valid2 in |- *; intros k1 k2 t ep e p1 p2; unfold sum in |- *;
  Simplify; simpl in |- *; auto; try elim (fusion_stable t); 
  simpl in |- *; intros;
  [ apply sum1; assumption
  | apply sum2; try assumption; apply sum4; assumption
- | rewrite Zplus_comm; apply sum2; try assumption; apply sum4; assumption
+ | rewrite plus_comm; apply sum2; try assumption; apply sum4; assumption
  | apply sum3; try assumption; apply sum4; assumption
- | elim_eq_Z k1 0; simpl in |- *; auto; elim (fusion_stable t); simpl in |- *;
-    intros; unfold Zne in |- *; apply sum5; assumption ].
+ | apply sum5; auto ].
 Qed.
 
 (* \paragraph{[O_EXACT_DIVIDE]}
    c'est une oper1 valide mais on préfère une substitution a ce point la *)
 
-Definition exact_divide (k : Z) (body : term) (t : nat)
+Definition exact_divide (k : int) (body : term) (t : nat)
   (prop : proposition) :=
   match prop with
-  | EqTerm (Tint Z0) b =>
-      match eq_term (scalar_norm t (body * Tint k)%term) b with
-      | true =>
-          match eq_Z k 0 with
-          | true => TrueTerm
-          | false => EqTerm (Tint 0) body
-          end
-      | false => TrueTerm
-      end
-  | NeqTerm (Tint Z0) b =>
-      match eq_term (scalar_norm t (body * Tint k)%term) b with
-      | true =>
-          match eq_Z k 0 with
-          | true => FalseTerm
-          | false => NeqTerm (Tint 0) body
-          end
-      | false => TrueTerm
-      end
+  | EqTerm (Tint Null) b =>
+      if beq Null 0 && 
+         eq_term (scalar_norm t (body * Tint k)%term) b && 
+         negb (beq k 0) 
+      then EqTerm (Tint 0) body
+      else TrueTerm
+  | NeqTerm (Tint Null) b =>
+      if beq Null 0 && 
+         eq_term (scalar_norm t (body * Tint k)%term) b &&
+         negb (beq k 0)
+      then NeqTerm (Tint 0) body
+      else TrueTerm
   | _ => TrueTerm
   end.
 
 Theorem exact_divide_valid :
- forall (k : Z) (t : term) (n : nat), valid1 (exact_divide k t n).
-
-
-unfold valid1, exact_divide in |- *; intros k1 k2 t ep e p1; Simplify;
- simpl in |- *; auto; elim_eq_term (scalar_norm t (k2 * Tint k1)%term) t1;
- simpl in |- *; auto; elim_eq_Z k1 0; simpl in |- *; 
- auto; intros H1 H2; elim H2; elim scalar_norm_stable;
- simpl in |- *; 
- [
- generalize H1; case (interp_term e k2); 
- try trivial;
- (case k1; simpl in |- *;
-   [ intros; absurd (0 = 0); assumption
-   | intros p2 p3 H3 H4; discriminate H4
-   | intros p2 p3 H3 H4; discriminate H4 ])
- |
- subst k1; rewrite Zmult_comm; simpl in *; intros; absurd (0=0); trivial
- |
- generalize H1; case (interp_term e k2); 
- try trivial; intros p2 p3 H3 H4; discriminate H4
+ forall (k : int) (t : term) (n : nat), valid1 (exact_divide k t n).
+Proof.
+ unfold valid1, exact_divide in |- *; intros k1 k2 t ep e p1; 
+ Simplify; simpl; auto; subst; 
+ rewrite <- scalar_norm_stable; simpl; intros;
+ [ destruct (mult_integral _ _ (sym_eq H0)); intuition
+ | contradict H0; rewrite <- H0, mult_0_l; auto
  ].
 Qed.
 
@@ -1889,61 +2381,51 @@ Qed.
   La preuve reprend le schéma de la précédente mais on
   est sur une opération de type valid1 et non sur une opération terminale. *)
 
-Definition divide_and_approx (k1 k2 : Z) (body : term) 
+Definition divide_and_approx (k1 k2 : int) (body : term) 
   (t : nat) (prop : proposition) :=
   match prop with
-  | LeqTerm (Tint Z0) b =>
-      match
-        eq_term (scalar_norm_add t (body * Tint k1 + Tint k2)%term) b
-      with
-      | true =>
-          match k1 ?= 0 with
-          | Gt =>
-              match k1 ?= k2 with
-              | Gt => LeqTerm (Tint 0) body
-              | _ => prop
-              end
-          | _ => prop
-          end
-      | false => prop
-      end
+  | LeqTerm (Tint Null) b =>
+      if beq Null 0 && 
+         eq_term (scalar_norm_add t (body * Tint k1 + Tint k2)%term) b &&
+         bgt k1 0 && 
+         bgt k1 k2 
+      then LeqTerm (Tint 0) body 
+      else prop
   | _ => prop
   end.
 
 Theorem divide_and_approx_valid :
- forall (k1 k2 : Z) (body : term) (t : nat),
+ forall (k1 k2 : int) (body : term) (t : nat),
  valid1 (divide_and_approx k1 k2 body t).
-
-unfold valid1, divide_and_approx in |- *; intros k1 k2 body t ep e p1;
- Simplify;
- elim_eq_term (scalar_norm_add t (body * Tint k1 + Tint k2)%term) t1;
- Simplify; auto; intro E; elim E; simpl in |- *;
- elim (scalar_norm_add_stable t e); simpl in |- *; 
- intro H1; apply Zmult_le_approx with (3 := H1); assumption.
+Proof.
+ unfold valid1, divide_and_approx in |- *; intros k1 k2 body t ep e p1;
+ Simplify; simpl; auto; subst;
+ elim (scalar_norm_add_stable t e); simpl in |- *.
+ intro H2; apply mult_le_approx with (3 := H2); assumption.
 Qed.
 
 (* \paragraph{[MERGE_EQ]} *)
 
 Definition merge_eq (t : nat) (prop1 prop2 : proposition) :=
   match prop1 with
-  | LeqTerm (Tint Z0) b1 =>
+  | LeqTerm (Tint Null) b1 =>
       match prop2 with
-      | LeqTerm (Tint Z0) b2 =>
-          match eq_term b1 (scalar_norm t (b2 * Tint (-1))%term) with
-          | true => EqTerm (Tint 0) b1
-          | false => TrueTerm
-          end
+      | LeqTerm (Tint Null') b2 =>
+          if beq Null 0 && beq Null' 0 &&
+             eq_term b1 (scalar_norm t (b2 * Tint (-(1)))%term) 
+          then EqTerm (Tint 0) b1
+          else TrueTerm
       | _ => TrueTerm
       end
   | _ => TrueTerm
   end.
 
 Theorem merge_eq_valid : forall n : nat, valid2 (merge_eq n).
-
-unfold valid2, merge_eq in |- *; intros n ep e p1 p2; Simplify; simpl in |- *;
+Proof.
+ unfold valid2, merge_eq in |- *; intros n ep e p1 p2; Simplify; simpl in |- *;
  auto; elim (scalar_norm_stable n e); simpl in |- *; 
  intros; symmetry  in |- *; apply OMEGA8 with (2 := H0);
- [ assumption | elim Zopp_eq_mult_neg_1; trivial ].
+ [ assumption | elim opp_eq_mult_neg_1; trivial ].
 Qed.
 
 
@@ -1952,36 +2434,39 @@ Qed.
 
 Definition constant_nul (i : nat) (h : hyps) :=
   match nth_hyps i h with
-  | NeqTerm (Tint Z0) (Tint Z0) => absurd
+  | NeqTerm (Tint Null) (Tint Null') => 
+      if beq Null Null' then absurd else h 
   | _ => h
   end.
 
 Theorem constant_nul_valid : forall i : nat, valid_hyps (constant_nul i).
-
-unfold valid_hyps, constant_nul in |- *; intros;
+Proof.
+ unfold valid_hyps, constant_nul in |- *; intros;
  generalize (nth_valid ep e i lp); Simplify; simpl in |- *;
- unfold Zne in |- *; intro H1; absurd (0 = 0); auto.
+ intro H1; absurd (0 = 0); intuition.
 Qed.
 
 (* \paragraph{[O_STATE]} *)
 
-Definition state (m : Z) (s : step) (prop1 prop2 : proposition) :=
+Definition state (m : int) (s : step) (prop1 prop2 : proposition) :=
   match prop1 with
-  | EqTerm (Tint Z0) b1 =>
+  | EqTerm (Tint Null) b1 =>
       match prop2 with
       | EqTerm b2 b3 =>
-          EqTerm (Tint 0) (rewrite s (b1 + (- b3 + b2) * Tint m)%term)
+          if beq Null 0 
+          then EqTerm (Tint 0) (rewrite s (b1 + (- b3 + b2) * Tint m)%term)
+          else TrueTerm
       | _ => TrueTerm
       end
   | _ => TrueTerm
   end.
 
-Theorem state_valid : forall (m : Z) (s : step), valid2 (state m s).
-
-unfold valid2 in |- *; intros m s ep e p1 p2; unfold state in |- *; Simplify;
+Theorem state_valid : forall (m : int) (s : step), valid2 (state m s).
+Proof.
+ unfold valid2 in |- *; intros m s ep e p1 p2; unfold state in |- *; Simplify;
  simpl in |- *; auto; elim (rewrite_stable s e); simpl in |- *; 
  intros H1 H2; elim H1.
- rewrite H2; rewrite Zplus_opp_l; simpl; reflexivity.
+ now rewrite H2, plus_opp_l, plus_0_l, mult_0_l.
 Qed.
 
 (* \subsubsection{Tactiques générant plusieurs but}
@@ -1991,11 +2476,13 @@ Qed.
 Definition split_ineq (i t : nat) (f1 f2 : hyps -> lhyps) 
   (l : hyps) :=
   match nth_hyps i l with
-  | NeqTerm (Tint Z0) b1 =>
-      f1 (LeqTerm (Tint 0) (add_norm t (b1 + Tint (-1))%term) :: l) ++
+  | NeqTerm (Tint Null) b1 =>
+      if beq Null 0 then 
+      f1 (LeqTerm (Tint 0) (add_norm t (b1 + Tint (-(1)))%term) :: l) ++
       f2
         (LeqTerm (Tint 0)
-           (scalar_norm_add t (b1 * Tint (-1) + Tint (-1))%term) :: l)
+           (scalar_norm_add t (b1 * Tint (-(1)) + Tint (-(1)))%term) :: l)
+       else l :: nil
   | _ => l :: nil
   end.
 
@@ -2003,17 +2490,18 @@ Theorem split_ineq_valid :
  forall (i t : nat) (f1 f2 : hyps -> lhyps),
  valid_list_hyps f1 ->
  valid_list_hyps f2 -> valid_list_hyps (split_ineq i t f1 f2).
-
-unfold valid_list_hyps, split_ineq in |- *; intros i t f1 f2 H1 H2 ep e lp H;
+Proof.
+ unfold valid_list_hyps, split_ineq in |- *; intros i t f1 f2 H1 H2 ep e lp H;
  generalize (nth_valid _ _ i _ H); case (nth_hyps i lp); 
  simpl in |- *; auto; intros t1 t2; case t1; simpl in |- *; 
- auto; intros z; case z; simpl in |- *; auto; intro H3; 
+ auto; intros z; simpl in |- *; auto; intro H3.
+ Simplify.
  apply append_valid; elim (OMEGA19 (interp_term e t2));
  [ intro H4; left; apply H1; simpl in |- *; elim (add_norm_stable t);
     simpl in |- *; auto
  | intro H4; right; apply H2; simpl in |- *; elim (scalar_norm_add_stable t);
     simpl in |- *; auto
- | generalize H3; unfold Zne, not in |- *; intros E1 E2; apply E1;
+ | generalize H3; unfold not in |- *; intros E1 E2; apply E1;
     symmetry  in |- *; trivial ].
 Qed.
 
@@ -2046,8 +2534,8 @@ Fixpoint execute_omega (t : t_omega) (l : hyps) {struct t} : lhyps :=
   end.
 
 Theorem omega_valid : forall t : t_omega, valid_list_hyps (execute_omega t).
-
-simple induction t; simpl in |- *;
+Proof.
+ simple induction t; simpl in |- *;
  [ unfold valid_list_hyps in |- *; simpl in |- *; intros; left;
     apply (constant_not_nul_valid n ep e lp H)
  | unfold valid_list_hyps in |- *; simpl in |- *; intros; left;
@@ -2058,7 +2546,7 @@ simple induction t; simpl in |- *;
      (apply_oper_1_valid m (divide_and_approx k1 k2 body n)
         (divide_and_approx_valid k1 k2 body n) ep e lp H)
  | unfold valid_list_hyps in |- *; simpl in |- *; intros; left;
-    apply (not_exact_divide_valid z z0 t0 n n0 ep e lp H)
+    apply (not_exact_divide_valid i i0 t0 n n0 ep e lp H)
  | unfold valid_list_hyps, valid_hyps in |- *;
     intros k body n t' Ht' m ep e lp H; apply Ht';
     apply
@@ -2101,36 +2589,30 @@ Definition move_right (s : step) (p : proposition) :=
   | EqTerm t1 t2 => EqTerm (Tint 0) (rewrite s (t1 + - t2)%term)
   | LeqTerm t1 t2 => LeqTerm (Tint 0) (rewrite s (t2 + - t1)%term)
   | GeqTerm t1 t2 => LeqTerm (Tint 0) (rewrite s (t1 + - t2)%term)
-  | LtTerm t1 t2 => LeqTerm (Tint 0) (rewrite s (t2 + Tint (-1) + - t1)%term)
-  | GtTerm t1 t2 => LeqTerm (Tint 0) (rewrite s (t1 + Tint (-1) + - t2)%term)
+  | LtTerm t1 t2 => LeqTerm (Tint 0) (rewrite s (t2 + Tint (-(1)) + - t1)%term)
+  | GtTerm t1 t2 => LeqTerm (Tint 0) (rewrite s (t1 + Tint (-(1)) + - t2)%term)
   | NeqTerm t1 t2 => NeqTerm (Tint 0) (rewrite s (t1 + - t2)%term)
   | p => p
   end.
 
-Theorem Zne_left_2 : forall x y : Z, Zne x y -> Zne 0 (x + - y).
-unfold Zne, not in |- *; intros x y H1 H2; apply H1;
- apply (Zplus_reg_l (- y)); rewrite Zplus_comm; elim H2; 
- rewrite Zplus_opp_l; trivial.
-Qed.
-
 Theorem move_right_valid : forall s : step, valid1 (move_right s).
-
-unfold valid1, move_right in |- *; intros s ep e p; Simplify; simpl in |- *;
+Proof.
+ unfold valid1, move_right in |- *; intros s ep e p; Simplify; simpl in |- *;
  elim (rewrite_stable s e); simpl in |- *;
- [ symmetry  in |- *; apply Zegal_left; assumption
- | intro; apply Zle_left; assumption
- | intro; apply Zge_left; assumption
- | intro; apply Zgt_left; assumption
- | intro; apply Zlt_left; assumption
- | intro; apply Zne_left_2; assumption ].
+ [ symmetry  in |- *; apply egal_left; assumption
+ | intro; apply le_left; assumption
+ | intro; apply le_left; rewrite <- ge_le_iff; assumption
+ | intro; apply lt_left; rewrite <- gt_lt_iff; assumption
+ | intro; apply lt_left; assumption
+ | intro; apply ne_left_2; assumption ].
 Qed.
 
 Definition do_normalize (i : nat) (s : step) := apply_oper_1 i (move_right s).
 
 Theorem do_normalize_valid :
  forall (i : nat) (s : step), valid_hyps (do_normalize i s).
-
-intros; unfold do_normalize in |- *; apply apply_oper_1_valid;
+Proof.
+ intros; unfold do_normalize in |- *; apply apply_oper_1_valid;
  apply move_right_valid.
 Qed.
 
@@ -2143,43 +2625,40 @@ Fixpoint do_normalize_list (l : list step) (i : nat)
 
 Theorem do_normalize_list_valid :
  forall (l : list step) (i : nat), valid_hyps (do_normalize_list l i).
-
-simple induction l; simpl in |- *; unfold valid_hyps in |- *;
+Proof.
+ simple induction l; simpl in |- *; unfold valid_hyps in |- *;
  [ auto
  | intros a l' Hl' i ep e lp H; unfold valid_hyps in Hl'; apply Hl';
     apply (do_normalize_valid i a ep e lp); assumption ].
 Qed.
 
 Theorem normalize_goal :
- forall (s : list step) (ep : PropList) (env : list Z) (l : hyps),
+ forall (s : list step) (ep : list Prop) (env : list int) (l : hyps),
  interp_goal ep env (do_normalize_list s 0 l) -> interp_goal ep env l.
-
-intros; apply valid_goal with (2 := H); apply do_normalize_list_valid.
+Proof.
+ intros; apply valid_goal with (2 := H); apply do_normalize_list_valid.
 Qed.
 
 (* \subsubsection{Exécution de la trace} *)
 
 Theorem execute_goal :
- forall (t : t_omega) (ep : PropList) (env : list Z) (l : hyps),
+ forall (t : t_omega) (ep : list Prop) (env : list int) (l : hyps),
  interp_list_goal ep env (execute_omega t l) -> interp_goal ep env l.
-
-intros; apply (goal_valid (execute_omega t) (omega_valid t) ep env l H).
+Proof.
+ intros; apply (goal_valid (execute_omega t) (omega_valid t) ep env l H).
 Qed.
 
 
 Theorem append_goal :
- forall (ep : PropList) (e : list Z) (l1 l2 : lhyps),
+ forall (ep : list Prop) (e : list int) (l1 l2 : lhyps),
  interp_list_goal ep e l1 /\ interp_list_goal ep e l2 ->
  interp_list_goal ep e (l1 ++ l2).
-
-intros ep e; simple induction l1;
+Proof.
+ intros ep e; simple induction l1;
  [ simpl in |- *; intros l2 (H1, H2); assumption
  | simpl in |- *; intros h1 t1 HR l2 ((H1, H2), H3); split; auto ].
-
 Qed.
 
-Require Import Decidable.
-
 (* A simple decidability checker : if the proposition belongs to the
    simple grammar describe below then it is decidable. Proof is by 
    induction and uses well known theorem about arithmetic and propositional
@@ -2203,30 +2682,29 @@ Fixpoint decidability (p : proposition) : bool :=
   end.
 
 Theorem decidable_correct :
- forall (ep : PropList) (e : list Z) (p : proposition),
+ forall (ep : list Prop) (e : list int) (p : proposition),
  decidability p = true -> decidable (interp_proposition ep e p).
-
-simple induction p; simpl in |- *; intros;
+Proof.
+ simple induction p; simpl in |- *; intros;
  [ apply dec_eq
- | apply dec_Zle
+ | apply dec_le
  | left; auto
  | right; unfold not in |- *; auto
  | apply dec_not; auto
- | apply dec_Zge
- | apply dec_Zgt
- | apply dec_Zlt
- | apply dec_Zne
+ | apply dec_ge
+ | apply dec_gt
+ | apply dec_lt
+ | apply dec_ne
  | apply dec_or; elim andb_prop with (1 := H1); auto
  | apply dec_and; elim andb_prop with (1 := H1); auto
  | apply dec_imp; elim andb_prop with (1 := H1); auto
  | discriminate H ].
-
 Qed.
 
 (* An interpretation function for a complete goal with an explicit
    conclusion. We use an intermediate fixpoint. *)
 
-Fixpoint interp_full_goal (envp : PropList) (env : list Z) 
+Fixpoint interp_full_goal (envp : list Prop) (env : list int) 
  (c : proposition) (l : hyps) {struct l} : Prop :=
   match l with
   | nil => interp_proposition envp env c
@@ -2234,7 +2712,7 @@ Fixpoint interp_full_goal (envp : PropList) (env : list Z)
       interp_proposition envp env p' -> interp_full_goal envp env c l'
   end.
 
-Definition interp_full (ep : PropList) (e : list Z) 
+Definition interp_full (ep : list Prop) (e : list int) 
   (lc : hyps * proposition) : Prop :=
   match lc with
   | (l, c) => interp_full_goal ep e c l
@@ -2244,12 +2722,11 @@ Definition interp_full (ep : PropList) (e : list Z)
    of its hypothesis and conclusion *)
 
 Theorem interp_full_false :
- forall (ep : PropList) (e : list Z) (l : hyps) (c : proposition),
+ forall (ep : list Prop) (e : list int) (l : hyps) (c : proposition),
  (interp_hyps ep e l -> interp_proposition ep e c) -> interp_full ep e (l, c).
-
-simple induction l; unfold interp_full in |- *; simpl in |- *;
+Proof.
+ simple induction l; unfold interp_full in |- *; simpl in |- *;
  [ auto | intros a l1 H1 c H2 H3; apply H1; auto ].
-
 Qed.
 
 (* Push the conclusion in the list of hypothesis using a double negation
@@ -2265,11 +2742,11 @@ Definition to_contradict (lc : hyps * proposition) :=
    hypothesis implies the original goal *)
 
 Theorem to_contradict_valid :
- forall (ep : PropList) (e : list Z) (lc : hyps * proposition),
+ forall (ep : list Prop) (e : list int) (lc : hyps * proposition),
  interp_goal ep e (to_contradict lc) -> interp_full ep e lc.
-
-intros ep e lc; case lc; intros l c; simpl in |- *;
- pattern (decidability c) in |- *; apply bool_ind2;
+Proof.
+ intros ep e lc; case lc; intros l c; simpl in |- *;
+ pattern (decidability c) in |- *; apply bool_eq_ind;
  [ simpl in |- *; intros H H1; apply interp_full_false; intros H2;
     apply not_not;
     [ apply decidable_correct; assumption
@@ -2333,19 +2810,19 @@ Fixpoint destructure_hyps (nn : nat) (ll : hyps) {struct nn} : lhyps :=
   end.
 
 Theorem map_cons_val :
- forall (ep : PropList) (e : list Z) (p : proposition) (l : lhyps),
+ forall (ep : list Prop) (e : list int) (p : proposition) (l : lhyps),
  interp_proposition ep e p ->
  interp_list_hyps ep e l -> interp_list_hyps ep e (map_cons _ p l).
-
-simple induction l; simpl in |- *; [ auto | intros; elim H1; intro H2; auto ].
+Proof.
+ simple induction l; simpl in |- *; [ auto | intros; elim H1; intro H2; auto ].
 Qed.
 
 Hint Resolve map_cons_val append_valid decidable_correct.
 
 Theorem destructure_hyps_valid :
  forall n : nat, valid_list_hyps (destructure_hyps n).
-
-simple induction n;
+Proof.
+ simple induction n;
  [ unfold valid_list_hyps in |- *; simpl in |- *; auto
  | unfold valid_list_hyps at 2 in |- *; intros n1 H ep e lp; case lp;
     [ simpl in |- *; auto
@@ -2358,7 +2835,7 @@ simple induction n;
            (simpl in |- *; intros; apply map_cons_val; simpl in |- *; elim H0;
              auto);
           [ simpl in |- *; intros p1 (H1, H2);
-             pattern (decidability p1) in |- *; apply bool_ind2; 
+             pattern (decidability p1) in |- *; apply bool_eq_ind; 
              intro H3;
              [ apply H; simpl in |- *; split;
                 [ apply not_not; auto | assumption ]
@@ -2366,7 +2843,7 @@ simple induction n;
           | simpl in |- *; intros p1 p2 (H1, H2); apply H; simpl in |- *;
              elim not_or with (1 := H1); auto
           | simpl in |- *; intros p1 p2 (H1, H2);
-             pattern (decidability p1) in |- *; apply bool_ind2; 
+             pattern (decidability p1) in |- *; apply bool_eq_ind; 
              intro H3;
              [ apply append_valid; elim not_and with (2 := H1);
                 [ intro; left; apply H; simpl in |- *; auto
@@ -2378,18 +2855,17 @@ simple induction n;
           apply H; simpl in |- *; auto
        | simpl in |- *; intros; apply H; simpl in |- *; tauto
        | simpl in |- *; intros p1 p2 (H1, H2);
-          pattern (decidability p1) in |- *; apply bool_ind2; 
+          pattern (decidability p1) in |- *; apply bool_eq_ind; 
           intro H3;
           [ apply append_valid; elim imp_simp with (2 := H1);
              [ intro H4; left; simpl in |- *; apply H; simpl in |- *; auto
              | intro H4; right; simpl in |- *; apply H; simpl in |- *; auto
              | auto ]
           | auto ] ] ] ].
-
 Qed.
 
 Definition prop_stable (f : proposition -> proposition) :=
-  forall (ep : PropList) (e : list Z) (p : proposition),
+  forall (ep : list Prop) (e : list int) (p : proposition),
   interp_proposition ep e p <-> interp_proposition ep e (f p).
 
 Definition p_apply_left (f : proposition -> proposition) 
@@ -2405,8 +2881,8 @@ Definition p_apply_left (f : proposition -> proposition)
 Theorem p_apply_left_stable :
  forall f : proposition -> proposition,
  prop_stable f -> prop_stable (p_apply_left f).
-
-unfold prop_stable in |- *; intros f H ep e p; split;
+Proof.
+ unfold prop_stable in |- *; intros f H ep e p; split;
  (case p; simpl in |- *; auto; intros p1; elim (H ep e p1); tauto).
 Qed.
 
@@ -2423,8 +2899,8 @@ Definition p_apply_right (f : proposition -> proposition)
 Theorem p_apply_right_stable :
  forall f : proposition -> proposition,
  prop_stable f -> prop_stable (p_apply_right f).
-
-unfold prop_stable in |- *; intros f H ep e p; split;
+Proof.
+ unfold prop_stable in |- *; intros f H ep e p; split;
  (case p; simpl in |- *; auto;
    [ intros p1; elim (H ep e p1); tauto
    | intros p1 p2; elim (H ep e p2); tauto
@@ -2447,67 +2923,55 @@ Definition p_invert (f : proposition -> proposition)
 Theorem p_invert_stable :
  forall f : proposition -> proposition,
  prop_stable f -> prop_stable (p_invert f).
-
-unfold prop_stable in |- *; intros f H ep e p; split;
+Proof.
+ unfold prop_stable in |- *; intros f H ep e p; split;
  (case p; simpl in |- *; auto;
    [ intros t1 t2; elim (H ep e (NeqTerm t1 t2)); simpl in |- *;
-      unfold Zne in |- *;
       generalize (dec_eq (interp_term e t1) (interp_term e t2));
       unfold decidable in |- *; tauto
    | intros t1 t2; elim (H ep e (GtTerm t1 t2)); simpl in |- *;
-      unfold Zgt in |- *;
-      generalize (dec_Zgt (interp_term e t1) (interp_term e t2));
-      unfold decidable, Zgt, Zle in |- *; tauto
+      generalize (dec_gt (interp_term e t1) (interp_term e t2));
+      unfold decidable in |- *; rewrite le_lt_iff, <- gt_lt_iff; tauto
    | intros t1 t2; elim (H ep e (LtTerm t1 t2)); simpl in |- *;
-      unfold Zlt in |- *;
-      generalize (dec_Zlt (interp_term e t1) (interp_term e t2));
-      unfold decidable, Zge in |- *; tauto
+      generalize (dec_lt (interp_term e t1) (interp_term e t2));
+      unfold decidable in |- *; rewrite ge_le_iff, le_lt_iff; tauto
    | intros t1 t2; elim (H ep e (LeqTerm t1 t2)); simpl in |- *;
-      generalize (dec_Zgt (interp_term e t1) (interp_term e t2));
-      unfold Zle, Zgt in |- *; unfold decidable in |- *; 
-      tauto
+      generalize (dec_gt (interp_term e t1) (interp_term e t2));
+      unfold decidable in |- *; repeat rewrite le_lt_iff;
+      repeat rewrite gt_lt_iff; tauto
    | intros t1 t2; elim (H ep e (GeqTerm t1 t2)); simpl in |- *;
-      generalize (dec_Zlt (interp_term e t1) (interp_term e t2));
-      unfold Zge, Zlt in |- *; unfold decidable in |- *; 
-      tauto
+      generalize (dec_lt (interp_term e t1) (interp_term e t2));
+      unfold decidable in |- *; repeat rewrite ge_le_iff;
+      repeat rewrite le_lt_iff; tauto
    | intros t1 t2; elim (H ep e (EqTerm t1 t2)); simpl in |- *;
       generalize (dec_eq (interp_term e t1) (interp_term e t2));
-      unfold decidable, Zne in |- *; tauto ]).
-Qed.
-
-Theorem Zlt_left_inv : forall x y : Z, 0 <= y + -1 + - x -> x < y.
-
-intros; apply Zsucc_lt_reg; apply Zle_lt_succ;
- apply (fun a b : Z => Zplus_le_reg_r a b (-1 + - x)); 
- rewrite Zplus_assoc; unfold Zsucc in |- *; rewrite (Zplus_assoc_reverse x);
- rewrite (Zplus_assoc y); simpl in |- *; rewrite Zplus_0_r;
- rewrite Zplus_opp_r; assumption.
+      unfold decidable; tauto ]).
 Qed.
 
 Theorem move_right_stable : forall s : step, prop_stable (move_right s).
-
-unfold move_right, prop_stable in |- *; intros s ep e p; split;
+Proof.
+ unfold move_right, prop_stable in |- *; intros s ep e p; split;
  [ Simplify; simpl in |- *; elim (rewrite_stable s e); simpl in |- *;
-    [ symmetry  in |- *; apply Zegal_left; assumption
-    | intro; apply Zle_left; assumption
-    | intro; apply Zge_left; assumption
-    | intro; apply Zgt_left; assumption
-    | intro; apply Zlt_left; assumption
-    | intro; apply Zne_left_2; assumption ]
+    [ symmetry  in |- *; apply egal_left; assumption
+    | intro; apply le_left; assumption
+    | intro; apply le_left; rewrite <- ge_le_iff; assumption
+    | intro; apply lt_left; rewrite <- gt_lt_iff; assumption
+    | intro; apply lt_left; assumption
+    | intro; apply ne_left_2; assumption ]
  | case p; simpl in |- *; intros; auto; generalize H; elim (rewrite_stable s);
     simpl in |- *; intro H1;
-    [ rewrite (Zplus_0_r_reverse (interp_term e t0)); rewrite H1;
-       rewrite Zplus_permute; rewrite Zplus_opp_r; 
-       rewrite Zplus_0_r; trivial
-    | apply (fun a b : Z => Zplus_le_reg_r a b (- interp_term e t));
-       rewrite Zplus_opp_r; assumption
-    | apply Zle_ge;
-       apply (fun a b : Z => Zplus_le_reg_r a b (- interp_term e t0));
-       rewrite Zplus_opp_r; assumption
-    | apply Zlt_gt; apply Zlt_left_inv; assumption
-    | apply Zlt_left_inv; assumption
-    | unfold Zne, not in |- *; unfold Zne in H1; intro H2; apply H1;
-       rewrite H2; rewrite Zplus_opp_r; trivial ] ].
+    [ rewrite (plus_0_r_reverse (interp_term e t0)); rewrite H1;
+       rewrite plus_permute; rewrite plus_opp_r; 
+       rewrite plus_0_r; trivial
+    | apply (fun a b => plus_le_reg_r a b (- interp_term e t));
+       rewrite plus_opp_r; assumption
+    | rewrite ge_le_iff;
+       apply (fun a b => plus_le_reg_r a b (- interp_term e t0));
+       rewrite plus_opp_r; assumption
+    | rewrite gt_lt_iff; apply lt_left_inv; assumption
+    | apply lt_left_inv; assumption
+    | unfold not in |- *; intro H2; apply H1;
+       rewrite H2; rewrite plus_opp_r; trivial ] ].
 Qed.
 
 
@@ -2521,9 +2985,8 @@ Fixpoint p_rewrite (s : p_step) : proposition -> proposition :=
   end.
 
 Theorem p_rewrite_stable : forall s : p_step, prop_stable (p_rewrite s).
-
-
-simple induction s; simpl in |- *;
+Proof.
+ simple induction s; simpl in |- *;
  [ intros; apply p_apply_left_stable; trivial
  | intros; apply p_apply_right_stable; trivial
  | intros; apply p_invert_stable; apply move_right_stable
@@ -2539,8 +3002,8 @@ Fixpoint normalize_hyps (l : list h_step) (lh : hyps) {struct l} : hyps :=
 
 Theorem normalize_hyps_valid :
  forall l : list h_step, valid_hyps (normalize_hyps l).
-
-simple induction l; unfold valid_hyps in |- *; simpl in |- *;
+Proof.
+ simple induction l; unfold valid_hyps in |- *; simpl in |- *;
  [ auto
  | intros n_s r; case n_s; intros n s H ep e lp H1; apply H;
     apply apply_oper_1_valid;
@@ -2550,10 +3013,10 @@ simple induction l; unfold valid_hyps in |- *; simpl in |- *;
 Qed.
 
 Theorem normalize_hyps_goal :
- forall (s : list h_step) (ep : PropList) (env : list Z) (l : hyps),
+ forall (s : list h_step) (ep : list Prop) (env : list int) (l : hyps),
  interp_goal ep env (normalize_hyps s l) -> interp_goal ep env l.
-
-intros; apply valid_goal with (2 := H); apply normalize_hyps_valid.
+Proof.
+ intros; apply valid_goal with (2 := H); apply normalize_hyps_valid.
 Qed.
 
 Fixpoint extract_hyp_pos (s : list direction) (p : proposition) {struct s} :
@@ -2604,18 +3067,18 @@ Fixpoint extract_hyp_pos (s : list direction) (p : proposition) {struct s} :
   end.
 
 Definition co_valid1 (f : proposition -> proposition) :=
-  forall (ep : PropList) (e : list Z) (p1 : proposition),
+  forall (ep : list Prop) (e : list int) (p1 : proposition),
   interp_proposition ep e (Tnot p1) -> interp_proposition ep e (f p1).
 
 Theorem extract_valid :
  forall s : list direction,
  valid1 (extract_hyp_pos s) /\ co_valid1 (extract_hyp_neg s).
-
-unfold valid1, co_valid1 in |- *; simple induction s;
+Proof.
+ unfold valid1, co_valid1 in |- *; simple induction s;
  [ split;
     [ simpl in |- *; auto
     | intros ep e p1; case p1; simpl in |- *; auto; intro p;
-       pattern (decidability p) in |- *; apply bool_ind2;
+       pattern (decidability p) in |- *; apply bool_eq_ind;
        [ intro H; generalize (decidable_correct ep e p H);
           unfold decidable in |- *; tauto
        | simpl in |- *; auto ] ]
@@ -2623,12 +3086,11 @@ unfold valid1, co_valid1 in |- *; simple induction s;
     case p; auto; simpl in |- *; intros;
     (apply H1; tauto) ||
       (apply H2; tauto) ||
-        (pattern (decidability p0) in |- *; apply bool_ind2;
+        (pattern (decidability p0) in |- *; apply bool_eq_ind;
           [ intro H3; generalize (decidable_correct ep e p0 H3);
              unfold decidable in |- *; intro H4; apply H1; 
              tauto
           | intro; tauto ]) ].
-
 Qed.
 
 Fixpoint decompose_solve (s : e_step) (h : hyps) {struct s} : lhyps :=
@@ -2655,13 +3117,13 @@ Fixpoint decompose_solve (s : e_step) (h : hyps) {struct s} : lhyps :=
 
 Theorem decompose_solve_valid :
  forall s : e_step, valid_list_goal (decompose_solve s).
-
-intro s; apply goal_valid; unfold valid_list_hyps in |- *; elim s;
+Proof.
+ intro s; apply goal_valid; unfold valid_list_hyps in |- *; elim s;
  simpl in |- *; intros;
  [ cut (interp_proposition ep e1 (extract_hyp_pos l (nth_hyps n lp)));
     [ case (extract_hyp_pos l (nth_hyps n lp)); simpl in |- *; auto;
        [ intro p; case p; simpl in |- *; auto; intros p1 p2 H2;
-          pattern (decidability p1) in |- *; apply bool_ind2;
+          pattern (decidability p1) in |- *; apply bool_eq_ind;
           [ intro H3; generalize (decidable_correct ep e1 p1 H3); intro H4;
              apply append_valid; elim H4; intro H5;
              [ right; apply H0; simpl in |- *; tauto
@@ -2671,7 +3133,7 @@ intro s; apply goal_valid; unfold valid_list_hyps in |- *; elim s;
           [ intros H3; left; apply H; simpl in |- *; auto
           | intros H3; right; apply H0; simpl in |- *; auto ] 
        | intros p1 p2 H2;
-         pattern (decidability p1) in |- *; apply bool_ind2;
+         pattern (decidability p1) in |- *; apply bool_eq_ind;
           [ intro H3; generalize (decidable_correct ep e1 p1 H3); intro H4;
              apply append_valid; elim H4; intro H5; 
              [ right; apply H0; simpl in |- *; tauto
@@ -2687,7 +3149,7 @@ Qed.
 (* \subsection{La dernière étape qui élimine tous les séquents inutiles} *)
 
 Definition valid_lhyps (f : lhyps -> lhyps) :=
-  forall (ep : PropList) (e : list Z) (lp : lhyps),
+  forall (ep : list Prop) (e : list int) (lp : lhyps),
   interp_list_hyps ep e lp -> interp_list_hyps ep e (f lp).
 
 Fixpoint reduce_lhyps (lp : lhyps) : lhyps :=
@@ -2698,8 +3160,8 @@ Fixpoint reduce_lhyps (lp : lhyps) : lhyps :=
   end.
 
 Theorem reduce_lhyps_valid : valid_lhyps reduce_lhyps.
-
-unfold valid_lhyps in |- *; intros ep e lp; elim lp;
+Proof.
+ unfold valid_lhyps in |- *; intros ep e lp; elim lp;
  [ simpl in |- *; auto
  | intros a l HR; elim a;
     [ simpl in |- *; tauto
@@ -2707,10 +3169,10 @@ unfold valid_lhyps in |- *; intros ep e lp; elim lp;
 Qed.
 
 Theorem do_reduce_lhyps :
- forall (envp : PropList) (env : list Z) (l : lhyps),
+ forall (envp : list Prop) (env : list int) (l : lhyps),
  interp_list_goal envp env (reduce_lhyps l) -> interp_list_goal envp env l.
-
-intros envp env l H; apply list_goal_to_hyps; intro H1;
+Proof.
+ intros envp env l H; apply list_goal_to_hyps; intro H1;
  apply list_hyps_to_goal with (1 := H); apply reduce_lhyps_valid; 
  assumption.
 Qed.
@@ -2719,13 +3181,13 @@ Definition concl_to_hyp (p : proposition) :=
   if decidability p then Tnot p else TrueTerm.
 
 Definition do_concl_to_hyp :
-  forall (envp : PropList) (env : list Z) (c : proposition) (l : hyps),
+  forall (envp : list Prop) (env : list int) (c : proposition) (l : hyps),
   interp_goal envp env (concl_to_hyp c :: l) ->
   interp_goal_concl c envp env l.
-
-simpl in |- *; intros envp env c l; induction l as [| a l Hrecl];
+Proof.
+ simpl in |- *; intros envp env c l; induction l as [| a l Hrecl];
  [ simpl in |- *; unfold concl_to_hyp in |- *;
-    pattern (decidability c) in |- *; apply bool_ind2;
+    pattern (decidability c) in |- *; apply bool_eq_ind;
     [ intro H; generalize (decidable_correct envp env c H);
        unfold decidable in |- *; simpl in |- *; tauto
     | simpl in |- *; intros H1 H2; elim H2; trivial ]
@@ -2737,12 +3199,19 @@ Definition omega_tactic (t1 : e_step) (t2 : list h_step)
   reduce_lhyps (decompose_solve t1 (normalize_hyps t2 (concl_to_hyp c :: l))).
 
 Theorem do_omega :
- forall (t1 : e_step) (t2 : list h_step) (envp : PropList) 
-   (env : list Z) (c : proposition) (l : hyps),
+ forall (t1 : e_step) (t2 : list h_step) (envp : list Prop) 
+   (env : list int) (c : proposition) (l : hyps),
  interp_list_goal envp env (omega_tactic t1 t2 c l) ->
  interp_goal_concl c envp env l.
-
-unfold omega_tactic in |- *; intros; apply do_concl_to_hyp;
+Proof.
+ unfold omega_tactic in |- *; intros; apply do_concl_to_hyp;
  apply (normalize_hyps_goal t2); apply (decompose_solve_valid t1);
  apply do_reduce_lhyps; assumption.
 Qed.
+
+End IntOmega.
+
+(* For now, the above modular construction is instanciated on Z, 
+   in order to retrieve the initial ROmega. *)
+
+Module ZOmega := IntOmega(Z_as_Int).
diff --git a/contrib/romega/const_omega.ml b/contrib/romega/const_omega.ml
index 69b4b2de..bdec6bf4 100644
--- a/contrib/romega/const_omega.ml
+++ b/contrib/romega/const_omega.ml
@@ -48,64 +48,16 @@ let dest_const_apply t =
     | _ -> raise Destruct
   in  Nametab.id_of_global ref, args
 
-let recognize_number t =
-  let rec loop t =
-    let f,l = dest_const_apply t in
-    match Names.string_of_id f,l with
-       "xI",[t] -> Bigint.add Bigint.one (Bigint.mult Bigint.two (loop t))
-     | "xO",[t] -> Bigint.mult Bigint.two (loop t)
-     | "xH",[] -> Bigint.one
-     | _ -> failwith "not a number" in
-  let f,l = dest_const_apply t in
-    match Names.string_of_id f,l with
-        "Zpos",[t] -> loop t
-      | "Zneg",[t] -> Bigint.neg (loop t)
-      | "Z0",[] -> Bigint.zero
-      | _ -> failwith "not a number";;
-
-
 let logic_dir = ["Coq";"Logic";"Decidable"]
 
 let coq_modules =
   Coqlib.init_modules @ [logic_dir] @ Coqlib.arith_modules @ Coqlib.zarith_base_modules
-    @ [["Coq"; "omega"; "OmegaLemmas"]]
     @ [["Coq"; "Lists"; "List"]]
     @ [module_refl_path]
-
+    @ [module_refl_path@["ZOmega"]]
 
 let constant = Coqlib.gen_constant_in_modules "Omega" coq_modules
 
-let coq_xH = lazy (constant "xH")
-let coq_xO = lazy (constant "xO")
-let coq_xI = lazy (constant "xI")
-let coq_Z0 = lazy (constant "Z0")
-let coq_Zpos = lazy (constant "Zpos")
-let coq_Zneg = lazy (constant "Zneg")
-let coq_Z = lazy (constant "Z")
-let coq_comparison = lazy (constant  "comparison")
-let coq_Gt = lazy (constant "Gt")
-let coq_Lt = lazy (constant "Lt")
-let coq_Eq = lazy (constant "Eq")
-let coq_Zplus = lazy (constant "Zplus")
-let coq_Zmult = lazy (constant  "Zmult")
-let coq_Zopp = lazy (constant "Zopp")
-
-let coq_Zminus = lazy (constant "Zminus")
-let coq_Zsucc = lazy (constant  "Zsucc")
-let coq_Zgt = lazy (constant "Zgt")
-let coq_Zle = lazy (constant "Zle")
-let coq_Z_of_nat = lazy (constant  "Z_of_nat")
-
-(* Peano *)
-let coq_le = lazy(constant "le")
-let coq_gt = lazy(constant "gt")
-
-(* Integers *)
-let coq_nat = lazy(constant "nat")
-let coq_S = lazy(constant "S")
-let coq_O = lazy(constant "O")
-let coq_minus = lazy(constant "minus")
-
 (* Logic *)
 let coq_eq = lazy(constant  "eq")
 let coq_refl_equal = lazy(constant  "refl_equal")
@@ -114,15 +66,9 @@ let coq_not = lazy(constant "not")
 let coq_or = lazy(constant "or")
 let coq_True = lazy(constant "True")
 let coq_False = lazy(constant "False")
-let coq_ex = lazy(constant "ex")
 let coq_I = lazy(constant "I")
 
-(* Lists *)
-let coq_cons =  lazy (constant "cons")
-let coq_nil =  lazy (constant "nil")
-
-let coq_pcons = lazy (constant "Pcons")
-let coq_pnil = lazy (constant "Pnil")
+(* ReflOmegaCore/ZOmega *)
 
 let coq_h_step = lazy (constant "h_step")
 let coq_pair_step = lazy (constant  "pair_step")
@@ -130,8 +76,6 @@ let coq_p_left = lazy (constant  "P_LEFT")
 let coq_p_right = lazy (constant  "P_RIGHT")
 let coq_p_invert = lazy (constant  "P_INVERT")
 let coq_p_step = lazy (constant  "P_STEP")
-let coq_p_nop = lazy (constant  "P_NOP")
-
 
 let coq_t_int = lazy (constant  "Tint")
 let coq_t_plus = lazy (constant  "Tplus")
@@ -140,6 +84,7 @@ let coq_t_opp = lazy (constant  "Topp")
 let coq_t_minus = lazy (constant  "Tminus")
 let coq_t_var = lazy (constant  "Tvar")
 
+let coq_proposition = lazy (constant  "proposition")
 let coq_p_eq = lazy (constant  "EqTerm")
 let coq_p_leq = lazy (constant  "LeqTerm")
 let coq_p_geq = lazy (constant  "GeqTerm")
@@ -154,14 +99,6 @@ let coq_p_and = lazy (constant  "Tand")
 let coq_p_imp = lazy (constant  "Timp")
 let coq_p_prop = lazy (constant  "Tprop")
 
-let coq_proposition = lazy (constant  "proposition")
-let coq_interp_sequent = lazy (constant  "interp_goal_concl")
-let coq_normalize_sequent = lazy (constant  "normalize_goal")
-let coq_execute_sequent = lazy (constant  "execute_goal")
-let coq_do_concl_to_hyp =  lazy (constant  "do_concl_to_hyp")
-let coq_sequent_to_hyps = lazy (constant  "goal_to_hyps")
-let coq_normalize_hyps_goal = lazy (constant  "normalize_hyps_goal")
-
 (* Constructors for shuffle tactic *)
 let coq_t_fusion =  lazy (constant  "t_fusion")
 let coq_f_equal =  lazy (constant  "F_equal")
@@ -170,7 +107,6 @@ let coq_f_left =  lazy (constant  "F_left")
 let coq_f_right =  lazy (constant  "F_right")
 
 (* Constructors for reordering tactics *)
-let coq_step = lazy (constant  "step")
 let coq_c_do_both = lazy (constant  "C_DO_BOTH")
 let coq_c_do_left = lazy (constant  "C_LEFT")
 let coq_c_do_right = lazy (constant  "C_RIGHT")
@@ -196,8 +132,7 @@ let coq_c_red4 = lazy (constant  "C_RED4")
 let coq_c_red5 = lazy (constant  "C_RED5")
 let coq_c_red6 = lazy (constant  "C_RED6")
 let coq_c_mult_opp_left = lazy (constant  "C_MULT_OPP_LEFT")
-let coq_c_mult_assoc_reduced = 
-  lazy (constant  "C_MULT_ASSOC_REDUCED")
+let coq_c_mult_assoc_reduced = lazy (constant  "C_MULT_ASSOC_REDUCED")
 let coq_c_minus = lazy (constant  "C_MINUS")
 let coq_c_mult_comm = lazy (constant  "C_MULT_COMM")
 
@@ -225,30 +160,11 @@ let coq_e_split = lazy  (constant  "E_SPLIT")
 let coq_e_extract = lazy  (constant  "E_EXTRACT")
 let coq_e_solve = lazy  (constant  "E_SOLVE")
 
-let coq_decompose_solve_valid = 
-  lazy (constant   "decompose_solve_valid")
-let coq_do_reduce_lhyps = lazy (constant   "do_reduce_lhyps")
+let coq_interp_sequent = lazy (constant  "interp_goal_concl")
 let coq_do_omega = lazy (constant  "do_omega")
 
 (* \subsection{Construction d'expressions} *)
 
-
-let mk_var v = Term.mkVar (Names.id_of_string v)
-let mk_plus t1 t2 = Term.mkApp (Lazy.force coq_Zplus,[|  t1; t2 |])
-let mk_times t1 t2 = Term.mkApp (Lazy.force coq_Zmult, [| t1; t2 |])
-let mk_minus t1 t2 = Term.mkApp (Lazy.force coq_Zminus, [| t1;t2 |])
-let mk_eq t1 t2 = Term.mkApp (Lazy.force coq_eq, [| Lazy.force coq_Z; t1; t2 |])
-let mk_le t1 t2 = Term.mkApp (Lazy.force coq_Zle, [|t1; t2 |])
-let mk_gt t1 t2 = Term.mkApp (Lazy.force coq_Zgt, [|t1; t2 |])
-let mk_inv t = Term.mkApp (Lazy.force coq_Zopp, [|t |])
-let mk_and t1 t2 =  Term.mkApp (Lazy.force coq_and, [|t1; t2 |])
-let mk_or t1 t2 =  Term.mkApp (Lazy.force coq_or, [|t1; t2 |])
-let mk_not t = Term.mkApp (Lazy.force coq_not, [|t |])
-let mk_eq_rel t1 t2 = Term.mkApp (Lazy.force coq_eq, [|
-				Lazy.force coq_comparison; t1; t2 |])
-let mk_inj t = Term.mkApp (Lazy.force coq_Z_of_nat, [|t |])
-
-
 let do_left t = 
   if t = Lazy.force coq_c_nop then Lazy.force coq_c_nop
   else Term.mkApp (Lazy.force coq_c_do_left, [|t |] )
@@ -272,27 +188,20 @@ let rec do_list = function
   | [x] -> x
   | (x::l) -> do_seq x (do_list l)
 
-let mk_integer n =
-  let rec loop n = 
-    if n=Bigint.one then Lazy.force coq_xH else
-      let (q,r) = Bigint.euclid n Bigint.two in
-      Term.mkApp
-        ((if r = Bigint.zero then Lazy.force coq_xO else Lazy.force coq_xI),
-	[| loop q |]) in
-    
-    if n = Bigint.zero then Lazy.force coq_Z0 
-    else
-      if Bigint.is_strictly_pos n then
-        Term.mkApp (Lazy.force coq_Zpos, [| loop n |])
-      else
-        Term.mkApp (Lazy.force coq_Zneg, [| loop (Bigint.neg n) |])
+(* Nat *)
 
-let mk_Z = mk_integer
+let coq_S = lazy(constant "S")
+let coq_O = lazy(constant "O")
 
 let rec mk_nat = function
   | 0 -> Lazy.force coq_O
   | n -> Term.mkApp (Lazy.force coq_S, [| mk_nat (n-1) |])
 
+(* Lists *)
+
+let coq_cons =  lazy (constant "cons")
+let coq_nil =  lazy (constant "nil")
+
 let mk_list typ l =
   let rec loop = function
     | [] ->
@@ -301,14 +210,141 @@ let mk_list typ l =
 	Term.mkApp (Lazy.force coq_cons, [|typ; step; loop l |]) in
   loop l
 
-let mk_plist l =
-  let rec loop = function
-    | [] ->
-	(Lazy.force coq_pnil)
-    | (step :: l) -> 
-	Term.mkApp (Lazy.force coq_pcons, [| step; loop l |]) in
-  loop l
-
+let mk_plist l = mk_list Term.mkProp l
 
 let mk_shuffle_list l = mk_list (Lazy.force coq_t_fusion) l
 
+
+type parse_term = 
+  | Tplus of Term.constr * Term.constr 
+  | Tmult of Term.constr * Term.constr
+  | Tminus of Term.constr * Term.constr
+  | Topp of Term.constr
+  | Tsucc of Term.constr
+  | Tnum of Bigint.bigint
+  | Tother 
+
+type parse_rel = 
+  | Req of Term.constr * Term.constr
+  | Rne of Term.constr * Term.constr
+  | Rlt of Term.constr * Term.constr
+  | Rle of Term.constr * Term.constr
+  | Rgt of Term.constr * Term.constr
+  | Rge of Term.constr * Term.constr
+  | Rtrue
+  | Rfalse
+  | Rnot of Term.constr
+  | Ror of Term.constr * Term.constr
+  | Rand of Term.constr * Term.constr
+  | Rimp of Term.constr * Term.constr
+  | Riff of Term.constr * Term.constr
+  | Rother
+
+let parse_logic_rel c = 
+ try match destructurate c with
+   | Kapp("True",[]) -> Rtrue
+   | Kapp("False",[]) -> Rfalse
+   | Kapp("not",[t]) -> Rnot t
+   | Kapp("or",[t1;t2]) -> Ror (t1,t2) 
+   | Kapp("and",[t1;t2]) -> Rand (t1,t2)
+   | Kimp(t1,t2) -> Rimp (t1,t2)
+   | Kapp("iff",[t1;t2]) -> Riff (t1,t2)
+   | _ -> Rother
+ with e when Logic.catchable_exception e -> Rother
+
+
+module type Int = sig
+  val typ : Term.constr Lazy.t
+  val plus : Term.constr Lazy.t 
+  val mult : Term.constr Lazy.t
+  val opp : Term.constr Lazy.t
+  val minus : Term.constr Lazy.t
+
+  val mk : Bigint.bigint -> Term.constr
+  val parse_term : Term.constr -> parse_term
+  val parse_rel : Proof_type.goal Tacmach.sigma -> Term.constr -> parse_rel
+  (* check whether t is built only with numbers and + * - *)
+  val is_scalar : Term.constr -> bool 
+end
+
+module Z : Int = struct 
+
+let typ = lazy (constant "Z")
+let plus = lazy (constant "Zplus")
+let mult = lazy (constant  "Zmult")
+let opp = lazy (constant "Zopp")
+let minus = lazy (constant "Zminus")
+
+let coq_xH = lazy (constant "xH")
+let coq_xO = lazy (constant "xO")
+let coq_xI = lazy (constant "xI")
+let coq_Z0 = lazy (constant "Z0")
+let coq_Zpos = lazy (constant "Zpos")
+let coq_Zneg = lazy (constant "Zneg")
+
+let recognize t =
+  let rec loop t =
+    let f,l = dest_const_apply t in
+    match Names.string_of_id f,l with
+       "xI",[t] -> Bigint.add Bigint.one (Bigint.mult Bigint.two (loop t))
+     | "xO",[t] -> Bigint.mult Bigint.two (loop t)
+     | "xH",[] -> Bigint.one
+     | _ -> failwith "not a number" in
+  let f,l = dest_const_apply t in
+    match Names.string_of_id f,l with
+        "Zpos",[t] -> loop t
+      | "Zneg",[t] -> Bigint.neg (loop t)
+      | "Z0",[] -> Bigint.zero
+      | _ -> failwith "not a number";;
+
+let rec mk_positive n = 
+  if n=Bigint.one then Lazy.force coq_xH 
+  else
+    let (q,r) = Bigint.euclid n Bigint.two in
+    Term.mkApp
+      ((if r = Bigint.zero then Lazy.force coq_xO else Lazy.force coq_xI),
+       [| mk_positive q |]) 
+
+let mk_Z n =
+  if n = Bigint.zero then Lazy.force coq_Z0 
+  else if Bigint.is_strictly_pos n then
+    Term.mkApp (Lazy.force coq_Zpos, [| mk_positive n |])
+  else
+    Term.mkApp (Lazy.force coq_Zneg, [| mk_positive (Bigint.neg n) |])
+
+let mk = mk_Z
+
+let parse_term t = 
+  try match destructurate t with
+    | Kapp("Zplus",[t1;t2]) -> Tplus (t1,t2)
+    | Kapp("Zminus",[t1;t2]) -> Tminus (t1,t2)
+    | 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
+  with e when Logic.catchable_exception e -> Tother
+    
+let parse_rel gl t = 
+  try match destructurate t with 
+    | Kapp("eq",[typ;t1;t2]) 
+      when destructurate (Tacmach.pf_nf gl typ) = Kapp("Z",[]) -> Req (t1,t2)
+    | Kapp("Zne",[t1;t2]) -> Rne (t1,t2)
+    | Kapp("Zle",[t1;t2]) -> Rle (t1,t2)
+    | Kapp("Zlt",[t1;t2]) -> Rlt (t1,t2)
+    | Kapp("Zge",[t1;t2]) -> Rge (t1,t2)
+    | Kapp("Zgt",[t1;t2]) -> Rgt (t1,t2)
+    | _ -> parse_logic_rel t 
+  with e when Logic.catchable_exception e -> Rother
+
+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"|"Zpred"),[t]) -> aux t
+    | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> let _ = recognize t in true
+    | _ -> false in
+  try aux t with _ -> false
+
+end
diff --git a/contrib/romega/const_omega.mli b/contrib/romega/const_omega.mli
new file mode 100644
index 00000000..0f00e918
--- /dev/null
+++ b/contrib/romega/const_omega.mli
@@ -0,0 +1,176 @@
+(*************************************************************************
+
+   PROJET RNRT Calife - 2001
+   Author: Pierre Crégut - France Télécom R&D
+   Licence : LGPL version 2.1
+
+ *************************************************************************)
+
+
+(** Coq objects used in romega *)
+
+(* from Logic *)
+val coq_refl_equal : Term.constr lazy_t
+val coq_and : Term.constr lazy_t
+val coq_not : Term.constr lazy_t
+val coq_or : Term.constr lazy_t
+val coq_True : Term.constr lazy_t
+val coq_False : Term.constr lazy_t
+val coq_I : Term.constr lazy_t
+
+(* from ReflOmegaCore/ZOmega *)
+val coq_h_step : Term.constr lazy_t
+val coq_pair_step : Term.constr lazy_t
+val coq_p_left : Term.constr lazy_t
+val coq_p_right : Term.constr lazy_t
+val coq_p_invert : Term.constr lazy_t
+val coq_p_step : Term.constr lazy_t
+
+val coq_t_int : Term.constr lazy_t
+val coq_t_plus : Term.constr lazy_t
+val coq_t_mult : Term.constr lazy_t
+val coq_t_opp : Term.constr lazy_t
+val coq_t_minus : Term.constr lazy_t
+val coq_t_var : Term.constr lazy_t
+
+val coq_proposition : Term.constr lazy_t
+val coq_p_eq : Term.constr lazy_t
+val coq_p_leq : Term.constr lazy_t
+val coq_p_geq : Term.constr lazy_t
+val coq_p_lt : Term.constr lazy_t
+val coq_p_gt : Term.constr lazy_t
+val coq_p_neq : Term.constr lazy_t
+val coq_p_true : Term.constr lazy_t
+val coq_p_false : Term.constr lazy_t
+val coq_p_not : Term.constr lazy_t
+val coq_p_or : Term.constr lazy_t
+val coq_p_and : Term.constr lazy_t
+val coq_p_imp : Term.constr lazy_t
+val coq_p_prop : Term.constr lazy_t
+
+val coq_f_equal : Term.constr lazy_t
+val coq_f_cancel : Term.constr lazy_t
+val coq_f_left : Term.constr lazy_t
+val coq_f_right : Term.constr lazy_t
+
+val coq_c_do_both : Term.constr lazy_t
+val coq_c_do_left : Term.constr lazy_t
+val coq_c_do_right : Term.constr lazy_t
+val coq_c_do_seq : Term.constr lazy_t
+val coq_c_nop : Term.constr lazy_t
+val coq_c_opp_plus : Term.constr lazy_t
+val coq_c_opp_opp : Term.constr lazy_t
+val coq_c_opp_mult_r : Term.constr lazy_t
+val coq_c_opp_one : Term.constr lazy_t
+val coq_c_reduce : Term.constr lazy_t
+val coq_c_mult_plus_distr : Term.constr lazy_t
+val coq_c_opp_left : Term.constr lazy_t
+val coq_c_mult_assoc_r : Term.constr lazy_t
+val coq_c_plus_assoc_r : Term.constr lazy_t
+val coq_c_plus_assoc_l : Term.constr lazy_t
+val coq_c_plus_permute : Term.constr lazy_t
+val coq_c_plus_comm : Term.constr lazy_t
+val coq_c_red0 : Term.constr lazy_t
+val coq_c_red1 : Term.constr lazy_t
+val coq_c_red2 : Term.constr lazy_t
+val coq_c_red3 : Term.constr lazy_t
+val coq_c_red4 : Term.constr lazy_t
+val coq_c_red5 : Term.constr lazy_t
+val coq_c_red6 : Term.constr lazy_t
+val coq_c_mult_opp_left : Term.constr lazy_t
+val coq_c_mult_assoc_reduced : Term.constr lazy_t
+val coq_c_minus : Term.constr lazy_t
+val coq_c_mult_comm : Term.constr lazy_t
+
+val coq_s_constant_not_nul : Term.constr lazy_t
+val coq_s_constant_neg : Term.constr lazy_t
+val coq_s_div_approx : Term.constr lazy_t
+val coq_s_not_exact_divide : Term.constr lazy_t
+val coq_s_exact_divide : Term.constr lazy_t
+val coq_s_sum : Term.constr lazy_t
+val coq_s_state : Term.constr lazy_t
+val coq_s_contradiction : Term.constr lazy_t
+val coq_s_merge_eq : Term.constr lazy_t
+val coq_s_split_ineq : Term.constr lazy_t
+val coq_s_constant_nul : Term.constr lazy_t
+val coq_s_negate_contradict : Term.constr lazy_t
+val coq_s_negate_contradict_inv : Term.constr lazy_t
+
+val coq_direction : Term.constr lazy_t
+val coq_d_left : Term.constr lazy_t
+val coq_d_right : Term.constr lazy_t
+val coq_d_mono : Term.constr lazy_t
+
+val coq_e_split : Term.constr lazy_t
+val coq_e_extract : Term.constr lazy_t
+val coq_e_solve : Term.constr lazy_t
+
+val coq_interp_sequent : Term.constr lazy_t
+val coq_do_omega : Term.constr lazy_t
+
+(** Building expressions *)
+
+val do_left : Term.constr -> Term.constr
+val do_right : Term.constr -> Term.constr
+val do_both : Term.constr -> Term.constr -> Term.constr
+val do_seq : Term.constr -> Term.constr -> Term.constr
+val do_list : Term.constr list -> Term.constr
+
+val mk_nat : int -> Term.constr
+val mk_list : Term.constr -> Term.constr list -> Term.constr
+val mk_plist : Term.types list -> Term.types
+val mk_shuffle_list : Term.constr list -> Term.constr
+
+(** Analyzing a coq term *)
+
+(* The generic result shape of the analysis of a term.
+   One-level depth, except when a number is found *)
+type parse_term =
+    Tplus of Term.constr * Term.constr
+  | Tmult of Term.constr * Term.constr
+  | Tminus of Term.constr * Term.constr
+  | Topp of Term.constr
+  | Tsucc of Term.constr
+  | Tnum of Bigint.bigint
+  | Tother
+
+(* The generic result shape of the analysis of a relation.
+   One-level depth. *)
+type parse_rel =
+    Req of Term.constr * Term.constr
+  | Rne of Term.constr * Term.constr
+  | Rlt of Term.constr * Term.constr
+  | Rle of Term.constr * Term.constr
+  | Rgt of Term.constr * Term.constr
+  | Rge of Term.constr * Term.constr
+  | Rtrue
+  | Rfalse
+  | Rnot of Term.constr
+  | Ror of Term.constr * Term.constr
+  | Rand of Term.constr * Term.constr
+  | Rimp of Term.constr * Term.constr
+  | Riff of Term.constr * Term.constr
+  | Rother
+
+(* A module factorizing what we should now about the number representation *)
+module type Int =
+  sig
+    (* the coq type of the numbers *)
+    val typ : Term.constr Lazy.t
+    (* the operations on the numbers *)
+    val plus : Term.constr Lazy.t
+    val mult : Term.constr Lazy.t
+    val opp : Term.constr Lazy.t
+    val minus : Term.constr Lazy.t
+    (* building a coq number *)
+    val mk : Bigint.bigint -> Term.constr
+    (* parsing a term (one level, except if a number is found) *)
+    val parse_term : Term.constr -> parse_term
+    (* parsing a relation expression, including = < <= >= > *)
+    val parse_rel : Proof_type.goal Tacmach.sigma -> Term.constr -> parse_rel
+    (* Is a particular term only made of numbers and + * - ? *) 
+    val is_scalar : Term.constr -> bool
+  end
+
+(* Currently, we only use Z numbers *)
+module Z : Int
diff --git a/contrib/romega/g_romega.ml4 b/contrib/romega/g_romega.ml4
index 7cfc50f8..39b6c210 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/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml
index e7e7b3c5..fc4f7a8f 100644
--- a/contrib/romega/refl_omega.ml
+++ b/contrib/romega/refl_omega.ml
@@ -6,10 +6,7 @@
 
  *************************************************************************)
 
-(* The addition on int, since it while be hidden soon by the one on BigInt *)
-
-let (+.) = (+)
-
+open Util
 open Const_omega
 module OmegaSolver = Omega.MakeOmegaSolver (Bigint)
 open OmegaSolver
@@ -26,65 +23,6 @@ let pp i = print_int i; print_newline (); flush stdout
 (* More readable than the prefix notation *)
 let (>>) = Tacticals.tclTHEN
 
-(* [list_index t l = i] \eqv $nth l i = t \wedge \forall j < i nth l j != t$ *)
-
-let list_index t = 
-  let rec loop i = function
-    | (u::l) -> if u = t then i else loop (succ i) l
-    | [] -> raise Not_found in
-  loop 0
-
-(* [list_uniq l = filter_i (x i -> nth l (i-1) != x) l] *)
-let list_uniq l  = 
-  let rec uniq = function
-      x :: ((y :: _) as l) when x = y -> uniq l
-    | x :: l -> x :: uniq l
-    | [] -> [] in
-  uniq (List.sort compare l)
-
-(* $\forall x. mem x  (list\_union l1 l2) \eqv x \in \{l1\} \cup \{l2\}$ *)
-let list_union l1 l2 =
-  let rec loop buf = function
-      x :: r -> if List.mem x l2 then loop buf r else loop (x :: buf) r
-    | [] -> buf in
-  loop l2 l1
-
-(* $\forall x. 
-      mem \;\; x \;\; (list\_intersect\;\; l1\;\;l2) \eqv x \in \{l1\} 
-       \cap \{l2\}$ *)
-let list_intersect l1 l2 =
-  let rec loop buf = function
-      x :: r -> if List.mem x l2 then loop (x::buf) r else loop buf r
-    | [] -> buf in
-  loop [] l1
-
-(* cartesian product. Elements are lists and are concatenated.
-   $cartesian [x_1 ... x_n] [y_1 ... y_p] = [x_1 @ y_1, x_2 @ y_1 ... x_n @ y_1 , x_1 @ y_2 ... x_n @ y_p]$ *)
-
-let rec cartesien l1 l2 =
-  let rec loop = function
-      (x2 :: r2) -> List.map (fun x1 -> x1 @ x2) l1 @ loop r2
-    | [] -> [] in
-  loop l2
-
-(* remove element e from list l *)
-let list_remove e l =
-  let rec loop = function
-      x :: l -> if x = e then loop l else x :: loop l
-    | [] -> [] in
-  loop l
-
-(* equivalent of the map function but no element is added when the function
-   raises an exception (and the computation silently continues) *)
-let map_exc f = 
-  let rec loop = function 
-    (x::l) -> 
-      begin match try Some (f x) with exc -> None with
-        Some v -> v :: loop l | None -> loop l
-      end
-    | [] -> [] in
-  loop 
-
 let mkApp = Term.mkApp
 
 (* \section{Types}
@@ -174,6 +112,7 @@ type environment = {
 (* \subsection{Solution tree}
    Définition d'une solution trouvée par Omega sous la forme d'un identifiant,
    d'un ensemble d'équation dont dépend la solution et d'une trace *)
+(* La liste des dépendances est triée et sans redondance *)
 type solution = {
   s_index : int;
   s_equa_deps : int list;
@@ -280,7 +219,7 @@ let unintern_omega env id =
    calcul des variables utiles. *)
 
 let add_reified_atom t env =
-  try list_index t env.terms
+  try list_index0 t env.terms
   with Not_found ->
     let i = List.length env.terms in
     env.terms <- env.terms @ [t]; i
@@ -291,7 +230,7 @@ let get_reified_atom env =
 (* \subsection{Gestion de l'environnement de proposition pour Omega} *)
 (* ajout d'une proposition *)
 let add_prop env t =
-  try list_index t env.props
+  try list_index0 t env.props
   with Not_found ->
     let i = List.length env.props in  env.props <- env.props @ [t]; i
 
@@ -362,13 +301,6 @@ let omega_of_oformula env kind =
 
 (* \subsection{Omega vers Oformula} *)
 
-let reified_of_atom env i =
-  try Hashtbl.find env.real_indices i
-  with Not_found -> 
-    Printf.printf "Atome %d non trouvé\n" i; 
-    Hashtbl.iter (fun k v -> Printf.printf "%d -> %d\n" k v) env.real_indices;
-    raise Not_found
-
 let rec oformula_of_omega env af = 
   let rec loop = function
     | ({v=v; c=n}::r) ->
@@ -382,20 +314,27 @@ let app f v = mkApp(Lazy.force f,v)
 
 let rec coq_of_formula env t =
   let rec loop = function
-  | Oplus (t1,t2) -> app coq_Zplus [| loop t1; loop t2 |]
-  | Oopp t -> app coq_Zopp [| loop t |]
-  | Omult(t1,t2) -> app coq_Zmult [| loop t1; loop t2 |]
-  | Oint v ->   mk_Z v
+  | Oplus (t1,t2) -> app Z.plus [| loop t1; loop t2 |]
+  | Oopp t -> app Z.opp [| loop t |]
+  | Omult(t1,t2) -> app Z.mult [| loop t1; loop t2 |]
+  | Oint v ->   Z.mk v
   | Oufo t -> loop t
   | Oatom var ->
       (* attention ne traite pas les nouvelles variables si on ne les
        * met pas dans env.term *)
       get_reified_atom env var
-  | Ominus(t1,t2) -> app coq_Zminus [| loop t1; loop t2 |] in
+  | Ominus(t1,t2) -> app Z.minus [| loop t1; loop t2 |] in
   loop t
 
 (* \subsection{Oformula vers COQ reifié} *)
 
+let reified_of_atom env i =
+  try Hashtbl.find env.real_indices i
+  with Not_found -> 
+    Printf.printf "Atome %d non trouvé\n" i; 
+    Hashtbl.iter (fun k v -> Printf.printf "%d -> %d\n" k v) env.real_indices;
+    raise Not_found
+
 let rec reified_of_formula env = function
   | Oplus (t1,t2) ->
       app coq_t_plus [| reified_of_formula env t1; reified_of_formula env t2 |]
@@ -403,7 +342,7 @@ let rec reified_of_formula env = function
       app coq_t_opp [| reified_of_formula env t |]
   | Omult(t1,t2) ->
       app coq_t_mult [| reified_of_formula env t1; reified_of_formula env t2 |]
-  | Oint v ->  app coq_t_int [| mk_Z v |]
+  | Oint v ->  app coq_t_int [| Z.mk v |]
   | Oufo t -> reified_of_formula env t
   | Oatom i -> app coq_t_var [| mk_nat (reified_of_atom env i) |]
   | Ominus(t1,t2) ->
@@ -448,12 +387,12 @@ let reified_of_proposition env f =
 
 let reified_of_omega env body constant = 
   let coeff_constant = 
-    app coq_t_int [| mk_Z constant |] in
+    app coq_t_int [| Z.mk constant |] in
   let mk_coeff {c=c; v=v} t =
     let coef = 
       app coq_t_mult 
 	[| reified_of_formula env (unintern_omega env v); 
-	   app coq_t_int [| mk_Z c |] |] in
+	   app coq_t_int [| Z.mk c |] |] in
     app coq_t_plus [|coef; t |] in
   List.fold_right mk_coeff body coeff_constant
 
@@ -469,22 +408,34 @@ Ces fonctions préparent les traces utilisées par la tactique réfléchie
 pour faire des opérations de normalisation sur les équations.  *)
 
 (* \subsection{Extractions des variables d'une équation} *)
-(* Extraction des variables d'une équation *)
+(* Extraction des variables d'une équation. *)
+(* Chaque fonction retourne une liste triée sans redondance *)
+
+let (@@) = list_merge_uniq compare
 
 let rec vars_of_formula = function
   | Oint _ -> []
-  | Oplus (e1,e2)  -> (vars_of_formula e1) @ (vars_of_formula e2)
-  | Omult (e1,e2)  -> (vars_of_formula e1) @ (vars_of_formula e2)
-  | Ominus (e1,e2) -> (vars_of_formula e1) @ (vars_of_formula e2)
-  | Oopp e -> (vars_of_formula e)
+  | Oplus (e1,e2) -> (vars_of_formula e1) @@ (vars_of_formula e2)
+  | Omult (e1,e2) -> (vars_of_formula e1) @@ (vars_of_formula e2)
+  | Ominus (e1,e2) -> (vars_of_formula e1) @@ (vars_of_formula e2)
+  | Oopp e -> vars_of_formula e
   | Oatom i -> [i]
   | Oufo _ -> []
 
-let vars_of_equations l =
-  let rec loop = function
-      e :: l -> vars_of_formula e.e_left @ vars_of_formula e.e_right @ loop l
-    | [] -> [] in
-  list_uniq (List.sort compare (loop l))
+let rec vars_of_equations = function
+  | [] -> [] 
+  | e::l -> 
+      (vars_of_formula e.e_left) @@
+      (vars_of_formula e.e_right) @@
+      (vars_of_equations l)
+
+let rec vars_of_prop = function 
+  | Pequa(_,e) -> vars_of_equations [e]
+  | Pnot p -> vars_of_prop p
+  | Por(_,p1,p2) -> (vars_of_prop p1) @@ (vars_of_prop p2)
+  | Pand(_,p1,p2) -> (vars_of_prop p1) @@ (vars_of_prop p2)
+  | Pimp(_,p1,p2) -> (vars_of_prop p1) @@ (vars_of_prop p2)
+  | Pprop _ | Ptrue | Pfalse -> []
 
 (* \subsection{Multiplication par un scalaire} *)
 
@@ -715,36 +666,23 @@ let normalize_equation env (negated,depends,origin,path) (oper,t1,t2) =
 
 (* \section{Compilation des hypothèses} *)
 
-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(("Zpos"|"Zneg"|"Z0"),_) -> let _ = recognize_number t in true
-    | _ -> false in
-  try aux t with _ -> false
-
 let rec oformula_of_constr env t =
-  try match destructurate t with
-  | Kapp("Zplus",[t1;t2]) -> binop env (fun x y -> Oplus(x,y)) t1 t2
-  | Kapp("Zminus",[t1;t2]) -> binop env (fun x y -> Ominus(x,y)) t1 t2
-  | Kapp("Zmult",[t1;t2]) when is_scalar t1 or is_scalar t2 ->
-      binop env (fun x y -> Omult(x,y)) t1 t2
-  | Kapp("Zopp",[t]) -> Oopp(oformula_of_constr env t)
-  | Kapp("Zsucc",[t]) -> Oplus(oformula_of_constr env t, Oint one)
-  | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> 
-      begin try Oint(recognize_number t)
-      with _ -> Oatom (add_reified_atom t env) end
-  | _ -> 
-      Oatom (add_reified_atom t env)
-  with e when Logic.catchable_exception e ->
-    Oatom (add_reified_atom t env)
-
-and  binop env c t1 t2 = 
-    let t1' = oformula_of_constr env t1 in
-    let t2' = oformula_of_constr env t2 in
-    c t1' t2'
-
-and  binprop env (neg2,depends,origin,path) 
+  match Z.parse_term t with 
+    | Tplus (t1,t2) -> binop env (fun x y -> Oplus(x,y)) t1 t2
+    | Tminus (t1,t2) -> binop env (fun x y -> Ominus(x,y)) t1 t2
+    | Tmult (t1,t2) when Z.is_scalar t1 || Z.is_scalar t2 -> 
+	binop env (fun x y -> Omult(x,y)) t1 t2
+    | Topp t -> Oopp(oformula_of_constr env t)
+    | Tsucc t -> Oplus(oformula_of_constr env t, Oint one)
+    | Tnum n -> Oint n
+    | _ -> Oatom (add_reified_atom t env)
+
+and binop env c t1 t2 = 
+  let t1' = oformula_of_constr env t1 in
+  let t2' = oformula_of_constr env t2 in
+  c t1' t2'
+
+and binprop env (neg2,depends,origin,path) 
              add_to_depends neg1 gl c t1 t2 =
   let i = new_connector_id env in
   let depends1 = if add_to_depends then Left i::depends else depends in
@@ -767,40 +705,32 @@ and mk_equation env ctxt c connector t1 t2 =
   Pequa (c,omega)
 
 and oproposition_of_constr env ((negated,depends,origin,path) as ctxt) gl c = 
-  try match destructurate c with
-    | Kapp("eq",[typ;t1;t2]) 
-      when destructurate (Tacmach.pf_nf gl typ) = Kapp("Z",[]) ->
-         mk_equation env ctxt c Eq t1 t2
-    | Kapp("Zne",[t1;t2]) -> 
-	mk_equation env ctxt c Neq t1 t2
-    | Kapp("Zle",[t1;t2]) -> 
-	mk_equation env ctxt c Leq t1 t2
-    | Kapp("Zlt",[t1;t2]) -> 
-	mk_equation env ctxt c Lt t1 t2
-    | Kapp("Zge",[t1;t2]) -> 
-	mk_equation env ctxt c Geq t1 t2
-    | Kapp("Zgt",[t1;t2]) -> 
-	mk_equation env ctxt c Gt t1 t2
-    | Kapp("True",[]) -> Ptrue
-    | Kapp("False",[]) -> Pfalse
-    | Kapp("not",[t]) ->
-       let t' = 
-	 oproposition_of_constr 
-	   env (not negated, depends, origin,(O_mono::path)) gl t in 
-       Pnot t'
-    | Kapp("or",[t1;t2]) ->  
+  match Z.parse_rel gl c with 
+    | Req (t1,t2) -> mk_equation env ctxt c Eq t1 t2
+    | Rne (t1,t2) -> mk_equation env ctxt c Neq t1 t2
+    | Rle (t1,t2) -> mk_equation env ctxt c Leq t1 t2
+    | Rlt (t1,t2) -> mk_equation env ctxt c Lt t1 t2
+    | Rge (t1,t2) -> mk_equation env ctxt c Geq t1 t2
+    | Rgt (t1,t2) -> mk_equation env ctxt c Gt t1 t2
+    | Rtrue -> Ptrue 
+    | Rfalse -> Pfalse
+    | Rnot t -> 
+	let t' = 
+	  oproposition_of_constr 
+	    env (not negated, depends, origin,(O_mono::path)) gl t in 
+	Pnot t'
+    | Ror (t1,t2) -> 
 	binprop env ctxt (not negated) negated gl (fun i x y -> Por(i,x,y)) t1 t2
-    | Kapp("and",[t1;t2]) ->
+    | Rand (t1,t2) -> 
 	binprop env ctxt negated negated gl
 	  (fun i x y -> Pand(i,x,y)) t1 t2
-    | Kimp(t1,t2) ->
+    | Rimp (t1,t2) ->
 	binprop env ctxt (not negated) (not negated) gl 
 	  (fun i x y -> Pimp(i,x,y)) t1 t2
-    | Kapp("iff",[t1;t2]) ->
+    | Riff (t1,t2) ->
 	binprop env ctxt negated negated gl 
 	  (fun i x y -> Pand(i,x,y)) (Term.mkArrow t1 t2) (Term.mkArrow t2 t1)
     | _ -> Pprop c
-  with e when Logic.catchable_exception e -> Pprop c
 
 (* Destructuration des hypothèses et de la conclusion *)
 
@@ -881,7 +811,7 @@ let destructurate_hyps syst =
       (i,t) :: l -> 
 	let l_syst1 = destructurate_pos_hyp i []  [] t in
 	let l_syst2 = loop l in
-	cartesien l_syst1 l_syst2
+	list_cartesian (@) l_syst1 l_syst2
     | [] -> [[]] in
   loop syst
 
@@ -924,9 +854,9 @@ let display_systems syst_list =
 let rec hyps_used_in_trace = function
   | act :: l -> 
       begin match act with
-	| HYP e -> e.id :: hyps_used_in_trace l
+	| HYP e -> [e.id] @@ (hyps_used_in_trace l)
 	| SPLIT_INEQ (_,(_,act1),(_,act2)) -> 
-	    hyps_used_in_trace act1 @ hyps_used_in_trace act2
+	    hyps_used_in_trace act1 @@ hyps_used_in_trace act2
 	| _ -> hyps_used_in_trace l
       end
   | [] -> []
@@ -950,14 +880,15 @@ let rec variable_stated_in_trace = function
 ;;
 
 let add_stated_equations env tree = 
-  let rec loop = function
-      Tree(_,t1,t2) -> 
-	list_union (loop t1) (loop t2)
-    | Leaf s -> variable_stated_in_trace s.s_trace in
   (* Il faut trier les variables par ordre d'introduction pour ne pas risquer
      de définir dans le mauvais ordre *)
   let stated_equations = 
-    List.sort (fun x y -> Pervasives.(-) x.st_var y.st_var) (loop tree) in
+    let cmpvar x y = Pervasives.(-) x.st_var y.st_var in 
+    let rec loop = function
+      | Tree(_,t1,t2) -> List.merge cmpvar (loop t1) (loop t2)
+      | Leaf s -> List.sort cmpvar (variable_stated_in_trace s.s_trace) 
+    in loop tree
+  in 
   let add_env st = 
     (* On retransforme la définition de v en formule reifiée *)
     let v_def = oformula_of_omega env st.st_def in
@@ -966,7 +897,7 @@ let add_stated_equations env tree =
     let coq_v = coq_of_formula env v_def in
     let v = add_reified_atom coq_v env in
     (* Le terme qu'il va falloir introduire *)
-    let term_to_generalize = app coq_refl_equal [|Lazy.force coq_Z; coq_v|] in
+    let term_to_generalize = app coq_refl_equal [|Lazy.force Z.typ; coq_v|] in
     (* sa représentation sous forme d'équation mais non réifié car on n'a pas
      * l'environnement pour le faire correctement *)
     let term_to_reify = (v_def,Oatom v) in
@@ -978,10 +909,15 @@ let add_stated_equations env tree =
 (* Calcule la liste des éclatements à réaliser sur les hypothèses 
    nécessaires pour extraire une liste d'équations donnée *)
 
+(* PL: experimentally, the result order of the following function seems 
+   _very_ crucial for efficiency. No idea why. Do not remove the List.rev
+   or modify the current semantics of Util.list_union (some elements of first 
+   arg, then second arg), unless you know what you're doing. *)
+
 let rec get_eclatement env = function
     i :: r -> 
       let l = try (get_equation env i).e_depends with Not_found -> [] in
-      list_union l (get_eclatement env r)
+      list_union (List.rev l) (get_eclatement env r)
   | [] -> []
 
 let select_smaller l = 
@@ -992,14 +928,13 @@ let filter_compatible_systems required systems =
   let rec select = function
       (x::l) -> 
 	if List.mem x required then select l
-	else if List.mem (barre x) required then raise Exit 
+	else if List.mem (barre x) required then failwith "Exit" 
 	else x :: select l
     | [] -> [] in
-  map_exc (function (sol,splits) -> (sol,select splits)) systems
+  map_succeed (function (sol,splits) -> (sol,select splits)) systems
 
 let rec equas_of_solution_tree = function
-    Tree(_,t1,t2) -> 
-      list_union (equas_of_solution_tree t1) (equas_of_solution_tree t2)
+    Tree(_,t1,t2) -> (equas_of_solution_tree t1)@@(equas_of_solution_tree t2)
   | Leaf s -> s.s_equa_deps
 
 (* [really_useful_prop] pushes useless props in a new Pprop variable *)
@@ -1041,14 +976,6 @@ let really_useful_prop l_equa c =
     None -> Pprop (real_of c)
   | Some t -> t
 
-let rec vars_of_prop = function 
-  | Pequa(_,e) -> vars_of_equations [e]
-  | Pnot p -> vars_of_prop p
-  | Por(_,p1,p2) -> list_union (vars_of_prop p1) (vars_of_prop p2)
-  | Pand(_,p1,p2) -> list_union (vars_of_prop p1) (vars_of_prop p2)
-  | Pimp(_,p1,p2) -> list_union (vars_of_prop p1) (vars_of_prop p2)
-  | _ -> []
-
 let rec display_solution_tree ch = function
     Leaf t -> 
       output_string ch 
@@ -1103,7 +1030,7 @@ let mk_direction_list l =
 (* \section{Rejouer l'historique} *)
 
 let get_hyp env_hyp i =
-  try list_index (CCEqua i) env_hyp
+  try list_index0 (CCEqua i) env_hyp
   with Not_found -> failwith (Printf.sprintf "get_hyp %d" i)
 
 let replay_history env env_hyp =
@@ -1116,7 +1043,7 @@ let replay_history env env_hyp =
 		    mk_nat (get_hyp env_hyp e2.id) |])
       | DIVIDE_AND_APPROX (e1,e2,k,d) :: l ->
 	  mkApp (Lazy.force coq_s_div_approx,
-		 [| mk_Z k; mk_Z d; 
+		 [| Z.mk k; Z.mk d; 
 		    reified_of_omega env e2.body e2.constant;
 		    mk_nat (List.length e2.body); 
 		    loop env_hyp l; mk_nat (get_hyp env_hyp e1.id) |])
@@ -1125,7 +1052,7 @@ let replay_history env env_hyp =
 	  let d = e1.constant - e2_constant * k in
 	  let e2_body = map_eq_linear (fun c -> c / k) e1.body in
           mkApp (Lazy.force coq_s_not_exact_divide,
-		 [|mk_Z k; mk_Z d; 
+		 [|Z.mk k; Z.mk d; 
 		   reified_of_omega env e2_body e2_constant; 
 		   mk_nat (List.length e2_body); 
 		   mk_nat (get_hyp env_hyp e1.id)|])
@@ -1134,7 +1061,7 @@ let replay_history env env_hyp =
 	    map_eq_linear (fun c -> c / k) e1.body in
 	  let e2_constant = floor_div e1.constant k in
           mkApp (Lazy.force coq_s_exact_divide,
-		 [|mk_Z k; 
+		 [|Z.mk k; 
 		   reified_of_omega env e2_body e2_constant; 
 		   mk_nat (List.length e2_body);
 		   loop env_hyp l; mk_nat (get_hyp env_hyp e1.id)|])
@@ -1149,7 +1076,7 @@ let replay_history env env_hyp =
 	  and n2 = get_hyp env_hyp e2.id in
 	  let trace = shuffle_path k1 e1.body k2 e2.body in
           mkApp (Lazy.force coq_s_sum,
-		 [| mk_Z k1; mk_nat n1; mk_Z k2;
+		 [| Z.mk k1; mk_nat n1; Z.mk k2;
 		    mk_nat n2; trace; (loop (CCEqua e3 :: env_hyp) l) |])
       | CONSTANT_NOT_NUL(e,k) :: l -> 
           mkApp (Lazy.force coq_s_constant_not_nul,
@@ -1169,7 +1096,7 @@ let replay_history env env_hyp =
 	     Oplus (o_orig,Omult (Oplus (Oopp v,o_def), Oint m)) in
           let trace,_ = normalize_linear_term env body in
 	  mkApp (Lazy.force coq_s_state,
-		 [| mk_Z m; trace; mk_nat n1; mk_nat n2; 
+		 [| Z.mk m; trace; mk_nat n1; mk_nat n2; 
 		    loop (CCEqua new_eq.id :: env_hyp) l |])
       |	HYP _ :: l -> loop env_hyp l
       |	CONSTANT_NUL e :: l ->
@@ -1267,17 +1194,17 @@ let resolution env full_reified_goal systems_list =
     print_newline()
   end;
   (* calcule la liste de toutes les hypothèses utilisées dans l'arbre de solution *)
-  let useful_equa_id = list_uniq (equas_of_solution_tree solution_tree) in
+  let useful_equa_id = equas_of_solution_tree solution_tree in
   (* recupere explicitement ces equations *)
   let equations = List.map (get_equation env) useful_equa_id in
-  let l_hyps' = list_uniq (List.map (fun e -> e.e_origin.o_hyp) equations) in
+  let l_hyps' = list_uniquize (List.map (fun e -> e.e_origin.o_hyp) equations) in
   let l_hyps = id_concl :: list_remove id_concl l_hyps' in
   let useful_hyps =
     List.map (fun id -> List.assoc id full_reified_goal) l_hyps in
   let useful_vars = 
     let really_useful_vars = vars_of_equations equations in
     let concl_vars = vars_of_prop (List.assoc id_concl full_reified_goal) in     
-    list_uniq (List.sort compare (really_useful_vars @ concl_vars))
+    really_useful_vars @@ concl_vars
   in 
   (* variables a introduire *)
   let to_introduce = add_stated_equations env solution_tree in
@@ -1295,7 +1222,7 @@ let resolution env full_reified_goal systems_list =
 	  Hashtbl.add env.real_indices var i; t :: loop (succ i) l
       |	[] -> [] in
     loop 0 all_vars_env in
-  let env_terms_reified = mk_list (Lazy.force coq_Z) basic_env in
+  let env_terms_reified = mk_list (Lazy.force Z.typ) basic_env in
   (* On peut maintenant généraliser le but : env est a jour *)
   let l_reified_stated =
      List.map (fun (_,_,(l,r),_) -> 
@@ -1325,10 +1252,10 @@ let resolution env full_reified_goal systems_list =
       |	((O_left | O_mono) :: l) -> app coq_p_left [| loop l |]
       |	(O_right :: l) -> app coq_p_right [| loop l |] in
     let correct_index = 
-      let i = list_index e.e_origin.o_hyp l_hyps in 
+      let i = list_index0 e.e_origin.o_hyp l_hyps in 
       (* PL: it seems that additionnally introduced hyps are in the way during 
              normalization, hence this index shifting... *) 
-      if i=0 then 0 else i +. List.length to_introduce
+      if i=0 then 0 else Pervasives.(+) i (List.length to_introduce)
     in 	
     app coq_pair_step [| mk_nat correct_index; loop e.e_origin.o_path |] in
   let normalization_trace =