Added transitivity and irreflexivity of <, as well as < -elimination for binary positive numbers.

Added directory contribs/micromega with the generalization of Frédéric Besson's micromega tactic for an arbitrary ordered ring. So far no tactic has been defined. One has to apply the theorems and find the certificate, which is necessary to solve inequations, manually.


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

20 files changed, 1729 insertions, 361 deletions

diff --git a/configure b/configure
index 7962f27d8..a8891856d 100755
--- a/configure
+++ b/configure
@@ -399,24 +399,24 @@ esac
 # Very basic for the moment: if camlp5 exists, we use it...
 
 if [ "$camlp5dir" != "" ]; then
-    CAMLP4=camlp5
+    CAMLP4=$camlp5dir
     CAMLP4LIB=$camlp5dir
     camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
 elif [ "$CAMLTAG" = "OCAML310" ]; then
     if [ -x "${CAMLLIB}/camlp5" ]; then 
-        CAMLP4LIB=+camlp5
+	CAMLP4=camlp5
     elif [ -x "${CAMLLIB}/site-lib/camlp5" ]; then 
-        CAMLP4LIB=+site-lib/camlp5
+	CAMLP4=site-lib/camlp5
     else
 	echo "Objective Caml 3.10 found but no Camlp5 installed."
 	echo "Configuration script failed!"
 	exit 1
     fi
-    CAMLP4=camlp5
+    CAMLP4LIB=+$CAMLP4
     camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
 else 
     CAMLP4=camlp4
-    CAMLP4LIB=+camlp4
+    CAMLP4LIB=+$CAMLP4
 fi
 
 if [ "$CAMLP4" = "camlp5" ] && `$camlp4oexec -v 2>&1 | grep -q 5.00`; then
diff --git a/contrib/micromega/CheckerMaker.v b/contrib/micromega/CheckerMaker.v
new file mode 100644
index 000000000..8aeada77b
--- /dev/null
+++ b/contrib/micromega/CheckerMaker.v
@@ -0,0 +1,121 @@
+(********************************************************************)
+(*                                                                  *)
+(* Micromega: A reflexive tactics using the Positivstellensatz      *)
+(*                                                                  *)
+(*  Frédéric Besson (Irisa/Inria) 2006				    *)
+(*                                                                  *)
+(********************************************************************)
+
+Require Import Decidable.
+Require Import List.
+Require Import Refl.
+
+Set Implicit Arguments.
+
+Section CheckerMaker.
+
+(* 'Formula' is a syntactic representation of a certain kind of propositions. *)
+Variable Formula : Type.
+
+Variable Env : Type.
+
+Variable eval : Env -> Formula -> Prop.
+
+Variable Formula' : Type.
+
+Variable eval' : Env -> Formula' -> Prop.
+
+Variable normalise : Formula -> Formula'.
+
+Variable negate : Formula -> Formula'.
+
+Hypothesis normalise_sound :
+  forall (env : Env) (t : Formula), eval env t -> eval' env (normalise t).
+
+Hypothesis negate_correct :
+  forall (env : Env) (t : Formula), eval env t <-> ~ (eval' env (negate t)).
+
+Variable Witness : Type.
+
+Variable check_formulas' : list Formula' -> Witness -> bool.
+
+Hypothesis check_formulas'_sound :
+  forall (l : list Formula') (w : Witness),
+    check_formulas' l w = true ->
+      forall env : Env, make_impl (eval' env) l False.
+
+Definition normalise_list : list Formula -> list Formula' := map normalise.
+Definition negate_list : list Formula -> list Formula' := map negate.
+
+Definition check_formulas (l : list Formula) (w : Witness) : bool :=
+  check_formulas' (map normalise l) w.
+
+(* Contraposition of normalise_sound for lists *)
+Lemma normalise_sound_contr : forall (env : Env) (l : list Formula),
+  make_impl (eval' env) (map normalise l) False -> make_impl (eval env) l False.
+Proof.
+intros env l; induction l as [| t l IH]; simpl in *.
+trivial.
+intros H1 H2. apply IH. apply H1. now apply normalise_sound.
+Qed.
+
+Theorem check_formulas_sound :
+  forall (l : list Formula) (w : Witness),
+    check_formulas l w = true -> forall env : Env, make_impl (eval env) l False.
+Proof.
+unfold check_formulas; intros l w H env. destruct l as [| t l]; simpl in *.
+pose proof (check_formulas'_sound H env) as H1; now simpl in H1.
+intro H1. apply normalise_sound in H1.
+pose proof (check_formulas'_sound H env) as H2; simpl in H2.
+apply H2 in H1. now apply normalise_sound_contr.
+Qed.
+
+(* In check_conj_formulas', t2 is supposed to be a list of negations of
+formulas. If, for example, t1 = [A1, A2] and t2 = [~ B1, ~ B2], then
+check_conj_formulas' checks that each of [~ B1, A1, A2] and [~ B2, A1, A2] is
+inconsistent. This means that A1 /\ A2 -> B1 and A1 /\ A2 -> B1, i.e., that
+A1 /\ A2 -> B1 /\ B2. *)
+
+Fixpoint check_conj_formulas'
+  (t1 : list Formula') (wits : list Witness) (t2 : list Formula') {struct wits} : bool :=
+match t2 with
+| nil => true
+| t':: rt2 =>
+  match wits with
+  | nil => false
+  | w :: rwits =>
+    match check_formulas' (t':: t1) w with
+    | true => check_conj_formulas' t1 rwits rt2
+    | false => false
+    end
+  end
+end.
+
+(* checks whether the conjunction of t1 implies the conjunction of t2 *)
+
+Definition check_conj_formulas
+  (t1 : list Formula) (wits : list Witness) (t2 : list Formula) : bool :=
+    check_conj_formulas' (normalise_list t1) wits (negate_list t2).
+
+Theorem check_conj_formulas_sound :
+  forall (t1 : list Formula) (t2 : list Formula) (wits : list Witness),
+    check_conj_formulas t1 wits t2 = true ->
+      forall env : Env, make_impl (eval env) t1 (make_conj (eval env) t2).
+Proof.
+intro t1; induction t2 as [| a2 t2' IH].
+intros; apply make_impl_true.
+intros wits H env.
+unfold check_conj_formulas in H; simpl in H.
+destruct wits as [| w ws]; simpl in H. discriminate.
+case_eq (check_formulas' (negate a2 :: normalise_list t1) w);
+intro H1; rewrite H1 in H; [| discriminate].
+assert (H2 : make_impl (eval' env) (negate a2 :: normalise_list t1) False) by
+now apply check_formulas'_sound with (w := w). clear H1.
+pose proof (IH ws H env) as H1. simpl in H2.
+assert (H3 : eval' env (negate a2) -> make_impl (eval env) t1 False)
+by auto using normalise_sound_contr. clear H2. rewrite <- make_conj_impl in *.
+rewrite make_conj_cons. intro H2. split.
+apply <- negate_correct. intro; now elim H3. exact (H1 H2).
+Qed.
+
+End CheckerMaker.
diff --git a/contrib/micromega/Examples.v b/contrib/micromega/Examples.v
new file mode 100644
index 000000000..976815142
--- /dev/null
+++ b/contrib/micromega/Examples.v
@@ -0,0 +1,103 @@
+Require Import OrderedRing.
+Require Import RingMicromega.
+Require Import Ring_polynom.
+Require Import ZCoeff.
+Require Import Refl.
+Require Import ZArith.
+Require Import List.
+
+Import OrderedRingSyntax.
+
+Section Examples.
+
+Variable R : Type.
+Variables rO rI : R.
+Variables rplus rtimes rminus: R -> R -> R.
+Variable ropp : R -> R.
+Variables req rle rlt : R -> R -> Prop.
+
+Variable sor : SOR rO rI rplus rtimes rminus ropp req rle rlt.
+
+Notation "0" := rO.
+Notation "1" := rI.
+Notation "x + y" := (rplus x y).
+Notation "x * y " := (rtimes x y).
+Notation "x - y " := (rminus x y).
+Notation "- x" := (ropp x).
+Notation "x == y" := (req x y).
+Notation "x ~= y" := (~ req x y).
+Notation "x <= y" := (rle x y).
+Notation "x < y" := (rlt x y).
+
+Definition phi : Z -> R := gen_order_phi_Z 0 1 rplus rtimes ropp.
+
+Lemma ZSORaddon :
+  SORaddon 0 1 rplus rtimes rminus ropp req rle (* ring elements *)
+           0%Z 1%Z Zplus Zmult Zminus Zopp (* coefficients *)
+           Zeq_bool Zle_bool
+           phi (fun x => x) (pow_N 1 rtimes).
+Proof.
+constructor.
+exact (Zring_morph sor).
+exact (pow_N_th 1 rtimes sor.(SORsetoid)).
+apply (Zcneqb_morph sor).
+apply (Zcleb_morph sor).
+Qed.
+
+Definition Zeval_formula :=
+  eval_formula 0 rplus rtimes rminus ropp req rle rlt phi (fun x => x) (pow_N 1 rtimes).
+Definition Z_In := S_In 0%Z Zeq_bool Zle_bool.
+Definition Z_Square := S_Square 0%Z Zeq_bool Zle_bool.
+
+(* Example: forall x y : Z, x + y = 0 -> x - y = 0 -> x < 0 -> False *)
+
+Lemma plus_minus : forall x y : R, x + y == 0 -> x - y == 0 -> x < 0 -> False.
+Proof.
+intros x y.
+Open Scope Z_scope.
+set (varmap := fun (x y : R) => x :: y :: nil).
+set (expr :=
+ Build_Formula (PEadd (PEX Z 1) (PEX Z 2)) OpEq (PEc 0)
+   :: Build_Formula (PEsub (PEX Z 1) (PEX Z 2)) OpEq (PEc 0)
+      :: Build_Formula (PEX Z 1) OpLt (PEc 0) :: nil).
+set (cert :=
+   S_Add (S_Mult (S_Pos 0 Zeq_bool Zle_bool 2 (refl_equal true)) (Z_In 2))
+     (S_Add (S_Ideal (PEc 1) (Z_In 1)) (S_Ideal (PEc 1) (Z_In 0)))).
+change (make_impl (Zeval_formula (varmap x y)) expr False).
+apply (check_formulas_sound sor ZSORaddon expr cert).
+reflexivity.
+Close Scope Z_scope.
+Qed.
+
+(* Example *)
+
+Let four : R := ((1 + 1) * (1 + 1)).
+Lemma Zdiscr :
+  forall a b c x : R,
+    a * (x * x) + b * x + c == 0 -> 0 <= b * b - four * a * c.
+Proof.
+Open Scope Z_scope.
+set (varmap := fun (a b c x : R) => a :: b :: c :: x:: nil).
+set (poly1 :=
+     (Build_Formula
+           (PEadd
+              (PEadd (PEmul (PEX Z 1) (PEmul (PEX Z 4) (PEX Z 4)))
+                 (PEmul (PEX Z 2) (PEX Z 4))) (PEX Z 3)) OpEq (PEc 0)) :: nil).
+set (poly2 :=
+     (Build_Formula
+        (PEsub (PEmul (PEX Z 2) (PEX Z 2))
+           (PEmul (PEmul (PEc 4) (PEX Z 1)) (PEX Z 3))) OpGe (PEc 0)) :: nil).
+set (wit :=
+    (S_Add (Z_In 0)
+       (S_Add (S_Ideal (PEmul (PEc (-4)) (PEX Z 1)) (Z_In 1))
+          (Z_Square
+             (PEadd (PEmul (PEc 2) (PEmul (PEX Z 1) (PEX Z 4))) (PEX Z 2))))) :: nil).
+intros a b c x.
+change (make_impl (Zeval_formula (varmap a b c x)) poly1
+  (make_conj (Zeval_formula (varmap a b c x)) poly2)).
+apply (check_conj_formulas_sound sor ZSORaddon poly1 poly2 wit).
+reflexivity.
+Qed.
+
+End Examples.
+
diff --git a/contrib/micromega/OrderedRing.v b/contrib/micromega/OrderedRing.v
new file mode 100644
index 000000000..ac1833a13
--- /dev/null
+++ b/contrib/micromega/OrderedRing.v
@@ -0,0 +1,443 @@
+Require Import Setoid.
+Require Import Ring.
+
+Set Implicit Arguments.
+
+Module Import OrderedRingSyntax.
+Export RingSyntax.
+
+Reserved Notation "x ~= y" (at level 70, no associativity).
+Reserved Notation "x [=] y" (at level 70, no associativity).
+Reserved Notation "x [~=] y" (at level 70, no associativity).
+Reserved Notation "x [<] y" (at level 70, no associativity).
+Reserved Notation "x [<=] y" (at level 70, no associativity).
+End OrderedRingSyntax.
+
+Section DEFINITIONS.
+
+Variable R : Type.
+Variable (rO rI : R) (rplus rtimes rminus: R -> R -> R) (ropp : R -> R).
+Variable req rle rlt : R -> R -> Prop.
+Notation "0" := rO.
+Notation "1" := rI.
+Notation "x + y" := (rplus x y).
+Notation "x * y " := (rtimes x y).
+Notation "x - y " := (rminus x y).
+Notation "- x" := (ropp x).
+Notation "x == y" := (req x y).
+Notation "x ~= y" := (~ req x y).
+Notation "x <= y" := (rle x y).
+Notation "x < y" := (rlt x y).
+
+Record SOR : Prop := mk_SOR_theory {
+  SORsetoid : Setoid_Theory R req;
+  SORplus_wd : forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 + y1 == x2 + y2;
+  SORtimes_wd : forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 * y1 == x2 * y2;
+  SORopp_wd : forall x1 x2, x1 == x2 ->  -x1 == -x2;
+  SORle_wd : forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> (x1 <= y1 <-> x2 <= y2);
+  SORlt_wd : forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> (x1 < y1 <-> x2 < y2);
+  SORrt : ring_theory rO rI rplus rtimes rminus ropp req;
+  SORle_refl : forall n : R, n <= n;
+  SORle_antisymm : forall n m : R, n <= m -> m <= n -> n == m;
+  SORle_trans : forall n m p : R, n <= m -> m <= p -> n <= p;
+  SORlt_le_neq : forall n m : R, n < m <-> n <= m /\ n ~= m;
+  SORlt_trichotomy : forall n m : R,  n < m \/ n == m \/ m < n;
+  SORplus_le_mono_l : forall n m p : R, n <= m -> p + n <= p + m;
+  SORtimes_pos_pos : forall n m : R, 0 < n -> 0 < m -> 0 < n * m;
+  SORneq_0_1 : 0 ~= 1
+}.
+
+(* We cannot use Relation_Definitions.order.ord_antisym and
+Relations_1.Antisymmetric because they refer to Leibniz equality *)
+
+End DEFINITIONS.
+
+Section STRICT_ORDERED_RING.
+
+Variable R : Type.
+Variable (rO rI : R) (rplus rtimes rminus: R -> R -> R) (ropp : R -> R).
+Variable req rle rlt : R -> R -> Prop.
+
+Variable sor : SOR rO rI rplus rtimes rminus ropp req rle rlt.
+
+Notation "0" := rO.
+Notation "1" := rI.
+Notation "x + y" := (rplus x y).
+Notation "x * y " := (rtimes x y).
+Notation "x - y " := (rminus x y).
+Notation "- x" := (ropp x).
+Notation "x == y" := (req x y).
+Notation "x ~= y" := (~ req x y).
+Notation "x <= y" := (rle x y).
+Notation "x < y" := (rlt x y).
+
+Add Relation R req
+  reflexivity proved by sor.(SORsetoid).(Seq_refl _ _)
+  symmetry proved by sor.(SORsetoid).(Seq_sym _ _)
+  transitivity proved by sor.(SORsetoid).(Seq_trans _ _)
+as sor_setoid.
+
+Add Morphism rplus with signature req ==> req ==> req as rplus_morph.
+Proof.
+exact sor.(SORplus_wd).
+Qed.
+Add Morphism rtimes with signature req ==> req ==> req as rtimes_morph.
+Proof.
+exact sor.(SORtimes_wd).
+Qed.
+Add Morphism ropp with signature req ==> req as ropp_morph.
+Proof.
+exact sor.(SORopp_wd).
+Qed.
+Add Morphism rle with signature req ==> req ==> iff as rle_morph.
+Proof.
+exact sor.(SORle_wd).
+Qed.
+Add Morphism rlt with signature req ==> req ==> iff as rlt_morph.
+Proof.
+exact sor.(SORlt_wd).
+Qed.
+
+Add Ring SOR : sor.(SORrt).
+
+Add Morphism rminus with signature req ==> req ==> req as rminus_morph.
+Proof.
+intros x1 x2 H1 y1 y2 H2.
+rewrite (sor.(SORrt).(Rsub_def) x1 y1).
+rewrite (sor.(SORrt).(Rsub_def) x2 y2).
+rewrite H1; now rewrite H2.
+Qed.
+
+Theorem Rneq_symm : forall n m : R, n ~= m -> m ~= n.
+Proof.
+intros n m H1 H2; rewrite H2 in H1; now apply H1.
+Qed.
+
+(* Propeties of plus, minus and opp *)
+
+Theorem Rplus_0_l : forall n : R, 0 + n == n.
+Proof.
+intro; ring.
+Qed.
+
+Theorem Rplus_0_r : forall n : R, n + 0 == n.
+Proof.
+intro; ring.
+Qed.
+
+Theorem Rtimes_0_r : forall n : R, n * 0 == 0.
+Proof.
+intro; ring.
+Qed.
+
+Theorem Rplus_comm : forall n m : R, n + m == m + n.
+Proof.
+intros; ring.
+Qed.
+
+Theorem Rtimes_0_l : forall n : R, 0 * n == 0.
+Proof.
+intro; ring.
+Qed.
+
+Theorem Rtimes_comm : forall n m : R, n * m == m * n.
+Proof.
+intros; ring.
+Qed.
+
+Theorem Rminus_eq_0 : forall n m : R, n - m == 0 <-> n == m.
+Proof.
+intros n m.
+split; intro H. setoid_replace n with ((n - m) + m) by ring. rewrite H. now rewrite Rplus_0_l.
+rewrite H; ring.
+Qed.
+
+Theorem Rplus_cancel_l : forall n m p : R, p + n == p + m <-> n == m.
+Proof.
+intros n m p; split; intro H.
+setoid_replace n with (- p + (p + n)) by ring.
+setoid_replace m with (- p + (p + m)) by ring. now rewrite H.
+now rewrite H.
+Qed.
+
+(* Relations *)
+
+Theorem Rle_refl : forall n : R, n <= n.
+Proof sor.(SORle_refl).
+
+Theorem Rle_antisymm : forall n m : R, n <= m -> m <= n -> n == m.
+Proof sor.(SORle_antisymm).
+
+Theorem Rle_trans : forall n m p : R, n <= m -> m <= p -> n <= p.
+Proof sor.(SORle_trans).
+
+Theorem Rlt_trichotomy : forall n m : R,  n < m \/ n == m \/ m < n.
+Proof sor.(SORlt_trichotomy).
+
+Theorem Rlt_le_neq : forall n m : R, n < m <-> n <= m /\ n ~= m.
+Proof sor.(SORlt_le_neq).
+
+Theorem Rneq_0_1 : 0 ~= 1.
+Proof sor.(SORneq_0_1).
+
+Theorem Req_em : forall n m : R, n == m \/ n ~= m.
+Proof.
+intros n m. destruct (Rlt_trichotomy n m) as [H | [H | H]]; try rewrite Rlt_le_neq in H.
+right; now destruct H.
+now left.
+right; apply Rneq_symm; now destruct H.
+Qed.
+
+Theorem Req_dne : forall n m : R, ~ ~ n == m <-> n == m.
+Proof.
+intros n m; destruct (Req_em n m) as [H | H].
+split; auto.
+split. intro H1; false_hyp H H1. auto.
+Qed.
+
+Theorem Rle_lt_eq : forall n m : R, n <= m <-> n < m \/ n == m.
+Proof.
+intros n m; rewrite Rlt_le_neq.
+split; [intro H | intros [[H1 H2] | H]].
+destruct (Req_em n m) as [H1 | H1]. now right. left; now split.
+assumption.
+rewrite H; apply Rle_refl.
+Qed.
+
+Ltac le_less := rewrite Rle_lt_eq; left; try assumption.
+Ltac le_equal := rewrite Rle_lt_eq; right; try reflexivity; try assumption.
+Ltac le_elim H := rewrite Rle_lt_eq in H; destruct H as [H | H].
+
+Theorem Rlt_trans : forall n m p : R, n < m -> m < p -> n < p.
+Proof.
+intros n m p; repeat rewrite Rlt_le_neq; intros [H1 H2] [H3 H4]; split.
+now apply Rle_trans with m.
+intro H. rewrite H in H1. pose proof (Rle_antisymm H3 H1). now apply H4.
+Qed.
+
+Theorem Rle_lt_trans : forall n m p : R, n <= m -> m < p -> n < p.
+Proof.
+intros n m p H1 H2; le_elim H1.
+now apply Rlt_trans with (m := m). now rewrite H1.
+Qed.
+
+Theorem Rlt_le_trans : forall n m p : R, n < m -> m <= p -> n < p.
+Proof.
+intros n m p H1 H2; le_elim H2.
+now apply Rlt_trans with (m := m). now rewrite <- H2.
+Qed.
+
+Theorem Rle_gt_cases : forall n m : R, n <= m \/ m < n.
+Proof.
+intros n m; destruct (Rlt_trichotomy n m) as [H | [H | H]].
+left; now le_less. left; now le_equal. now right.
+Qed.
+
+Theorem Rlt_neq : forall n m : R, n < m -> n ~= m.
+Proof.
+intros n m; rewrite Rlt_le_neq; now intros [_ H].
+Qed.
+
+Theorem Rle_ngt : forall n m : R, n <= m <-> ~ m < n.
+Proof.
+intros n m; split.
+intros H H1; assert (H2 : n < n) by now apply Rle_lt_trans with m. now apply (Rlt_neq H2).
+intro H. destruct (Rle_gt_cases n m) as [H1 | H1]. assumption. false_hyp H1 H.
+Qed.
+
+Theorem Rlt_nge : forall n m : R, n < m <-> ~ m <= n.
+Proof.
+intros n m; split.
+intros H H1; assert (H2 : n < n) by now apply Rlt_le_trans with m. now apply (Rlt_neq H2).
+intro H. destruct (Rle_gt_cases m n) as [H1 | H1]. false_hyp H1 H. assumption.
+Qed.
+
+(* Plus, minus and order *)
+
+Theorem Rplus_le_mono_l : forall n m p : R, n <= m <-> p + n <= p + m.
+Proof.
+intros n m p; split.
+apply sor.(SORplus_le_mono_l).
+intro H. apply (sor.(SORplus_le_mono_l) (p + n) (p + m) (- p)) in H.
+setoid_replace (- p + (p + n)) with n in H by ring.
+setoid_replace (- p + (p + m)) with m in H by ring. assumption.
+Qed.
+
+Theorem Rplus_le_mono_r : forall n m p : R, n <= m <-> n + p <= m + p.
+Proof.
+intros n m p; rewrite (Rplus_comm n p); rewrite (Rplus_comm m p).
+apply Rplus_le_mono_l.
+Qed.
+
+Theorem Rplus_lt_mono_l : forall n m p : R, n < m <-> p + n < p + m.
+Proof.
+intros n m p; do 2 rewrite Rlt_le_neq. rewrite Rplus_cancel_l.
+now rewrite <- Rplus_le_mono_l.
+Qed.
+
+Theorem Rplus_lt_mono_r : forall n m p : R, n < m <-> n + p < m + p.
+Proof.
+intros n m p.
+rewrite (Rplus_comm n p); rewrite (Rplus_comm m p); apply Rplus_lt_mono_l.
+Qed.
+
+Theorem Rplus_lt_mono : forall n m p q : R, n < m -> p < q -> n + p < m + q.
+Proof.
+intros n m p q H1 H2.
+apply Rlt_trans with (m + p); [now apply -> Rplus_lt_mono_r | now apply -> Rplus_lt_mono_l].
+Qed.
+
+Theorem Rplus_le_mono : forall n m p q : R, n <= m -> p <= q -> n + p <= m + q.
+Proof.
+intros n m p q H1 H2.
+apply Rle_trans with (m + p); [now apply -> Rplus_le_mono_r | now apply -> Rplus_le_mono_l].
+Qed.
+
+Theorem Rplus_lt_le_mono : forall n m p q : R, n < m -> p <= q -> n + p < m + q.
+Proof.
+intros n m p q H1 H2.
+apply Rlt_le_trans with (m + p); [now apply -> Rplus_lt_mono_r | now apply -> Rplus_le_mono_l].
+Qed.
+
+Theorem Rplus_le_lt_mono : forall n m p q : R, n <= m -> p < q -> n + p < m + q.
+Proof.
+intros n m p q H1 H2.
+apply Rle_lt_trans with (m + p); [now apply -> Rplus_le_mono_r | now apply -> Rplus_lt_mono_l].
+Qed.
+
+Theorem Rplus_pos_pos : forall n m : R, 0 < n -> 0 < m -> 0 < n + m.
+Proof.
+intros n m H1 H2. rewrite <- (Rplus_0_l 0). now apply Rplus_lt_mono.
+Qed.
+
+Theorem Rplus_pos_nonneg : forall n m : R, 0 < n -> 0 <= m -> 0 < n + m.
+Proof.
+intros n m H1 H2. rewrite <- (Rplus_0_l 0). now apply Rplus_lt_le_mono.
+Qed.
+
+Theorem Rplus_nonneg_pos : forall n m : R, 0 <= n -> 0 < m -> 0 < n + m.
+Proof.
+intros n m H1 H2. rewrite <- (Rplus_0_l 0). now apply Rplus_le_lt_mono.
+Qed.
+
+Theorem Rplus_nonneg_nonneg : forall n m : R, 0 <= n -> 0 <= m -> 0 <= n + m.
+Proof.
+intros n m H1 H2. rewrite <- (Rplus_0_l 0). now apply Rplus_le_mono.
+Qed.
+
+Theorem Rle_le_minus : forall n m : R, n <= m <-> 0 <= m - n.
+Proof.
+intros n m. rewrite (@Rplus_le_mono_r n m (- n)).
+setoid_replace (n + - n) with 0 by ring.
+now setoid_replace (m + - n) with (m - n) by ring.
+Qed.
+
+Theorem Rlt_lt_minus : forall n m : R, n < m <-> 0 < m - n.
+Proof.
+intros n m. rewrite (@Rplus_lt_mono_r n m (- n)).
+setoid_replace (n + - n) with 0 by ring.
+now setoid_replace (m + - n) with (m - n) by ring.
+Qed.
+
+Theorem Ropp_lt_mono : forall n m : R, n < m <-> - m < - n.
+Proof.
+intros n m. split; intro H.
+apply -> (@Rplus_lt_mono_l n m (- n - m)) in H.
+setoid_replace (- n - m + n) with (- m) in H by ring.
+now setoid_replace (- n - m + m) with (- n) in H by ring.
+apply -> (@Rplus_lt_mono_l (- m) (- n) (n + m)) in H.
+setoid_replace (n + m + - m) with n in H by ring.
+now setoid_replace (n + m + - n) with m in H by ring.
+Qed.
+
+Theorem Ropp_pos_neg : forall n : R, 0 < - n <-> n < 0.
+Proof.
+intro n; rewrite (Ropp_lt_mono n 0). now setoid_replace (- 0) with 0 by ring.
+Qed.
+
+(* Times and order *)
+
+Theorem Rtimes_pos_pos : forall n m : R, 0 < n -> 0 < m -> 0 < n * m.
+Proof sor.(SORtimes_pos_pos).
+
+Theorem Rtimes_nonneg_nonneg : forall n m : R, 0 <= n -> 0 <= m -> 0 <= n * m.
+Proof.
+intros n m H1 H2.
+le_elim H1. le_elim H2.
+le_less; now apply Rtimes_pos_pos.
+rewrite <- H2; rewrite Rtimes_0_r; le_equal.
+rewrite <- H1; rewrite Rtimes_0_l; le_equal.
+Qed.
+
+Theorem Rtimes_pos_neg : forall n m : R, 0 < n -> m < 0 -> n * m < 0.
+Proof.
+intros n m H1 H2. apply -> Ropp_pos_neg.
+setoid_replace (- (n * m)) with (n * (- m)) by ring.
+apply Rtimes_pos_pos. assumption. now apply <- Ropp_pos_neg.
+Qed.
+
+Theorem Rtimes_neg_neg : forall n m : R, n < 0 -> m < 0 -> 0 < n * m.
+Proof.
+intros n m H1 H2.
+setoid_replace (n * m) with ((- n) * (- m)) by ring.
+apply Rtimes_pos_pos; now apply <- Ropp_pos_neg.
+Qed.
+
+Theorem Rtimes_square_nonneg : forall n : R, 0 <= n * n.
+Proof.
+intro n; destruct (Rlt_trichotomy 0 n) as [H | [H | H]].
+le_less; now apply Rtimes_pos_pos.
+rewrite <- H, Rtimes_0_l; le_equal.
+le_less; now apply Rtimes_neg_neg.
+Qed.
+
+Theorem Rtimes_neq_0 : forall n m : R, n ~= 0 /\ m ~= 0 -> n * m ~= 0.
+Proof.
+intros n m [H1 H2].
+destruct (Rlt_trichotomy n 0) as [H3 | [H3 | H3]];
+destruct (Rlt_trichotomy m 0) as [H4 | [H4 | H4]];
+try (false_hyp H3 H1); try (false_hyp H4 H2).
+apply Rneq_symm. apply Rlt_neq. now apply Rtimes_neg_neg.
+apply Rlt_neq. rewrite Rtimes_comm. now apply Rtimes_pos_neg.
+apply Rlt_neq. now apply Rtimes_pos_neg.
+apply Rneq_symm. apply Rlt_neq. now apply Rtimes_pos_pos.
+Qed.
+
+(* The following theorems are used to build a morphism from Z to R and
+prove its properties in ZCoeff.v. They are not used in RingMicromega.v. *)
+
+(* Surprisingly, multilication is needed to prove the following theorem *)
+
+Theorem Ropp_neg_pos : forall n : R, - n < 0 <-> 0 < n.
+Proof.
+intro n; setoid_replace n with (- - n) by ring. rewrite Ropp_pos_neg.
+now setoid_replace (- - n) with n by ring.
+Qed.
+
+Theorem Rlt_0_1 : 0 < 1.
+Proof.
+apply <- Rlt_le_neq. split.
+setoid_replace 1 with (1 * 1) by ring; apply Rtimes_square_nonneg.
+apply Rneq_0_1.
+Qed.
+
+Theorem Rlt_succ_r : forall n : R, n < 1 + n.
+Proof.
+intro n. rewrite <- (Rplus_0_l n); setoid_replace (1 + (0 + n)) with (1 + n) by ring.
+apply -> Rplus_lt_mono_r. apply Rlt_0_1.
+Qed.
+
+Theorem Rlt_lt_succ : forall n m : R, n < m -> n < 1 + m.
+Proof.
+intros n m H; apply Rlt_trans with m. assumption. apply Rlt_succ_r.
+Qed.
+
+(*Theorem Rtimes_lt_mono_pos_l : forall n m p : R, 0 < p -> n < m -> p * n < p * m.
+Proof.
+intros n m p H1 H2. apply <- Rlt_lt_minus.
+setoid_replace (p * m - p * n) with (p * (m - n)) by ring.
+apply Rtimes_pos_pos. assumption. now apply -> Rlt_lt_minus.
+Qed.*)
+
+End STRICT_ORDERED_RING.
+
diff --git a/contrib/micromega/Refl.v b/contrib/micromega/Refl.v
new file mode 100644
index 000000000..8dced223b
--- /dev/null
+++ b/contrib/micromega/Refl.v
@@ -0,0 +1,74 @@
+(********************************************************************)
+(*                                                                  *)
+(* Micromega: A reflexive tactics using the Positivstellensatz *)
+(*                                                                  *)
+(*  Frédéric Besson (Irisa/Inria) 2006				    *)
+(*                                                                  *)
+(********************************************************************)
+Require Import List.
+
+Set Implicit Arguments.
+
+(* Refl of '->' '/\': basic properties *)
+
+Fixpoint make_impl (A : Type) (eval : A -> Prop) (l : list A) (goal : Prop) {struct l} : Prop :=
+  match l with
+    | nil => goal
+    | cons e l => (eval e) -> (make_impl eval l goal)
+  end.
+
+Theorem make_impl_true :
+  forall (A : Type) (eval : A -> Prop) (l : list A), make_impl eval l True.
+Proof.
+induction l as [| a l IH]; simpl.
+trivial.
+intro; apply IH.
+Qed.
+
+Fixpoint make_conj (A : Type) (eval : A -> Prop) (l : list A) {struct l} : Prop :=
+  match l with
+    | nil => True
+    | cons e nil => (eval e)
+    | cons e l2 => ((eval e) /\ (make_conj eval l2))
+  end.
+
+Theorem make_conj_cons : forall (A : Type) (eval : A -> Prop) (a : A) (l : list A),
+  make_conj eval (a :: l) <-> eval a /\ make_conj eval l.
+Proof.
+intros; destruct l; simpl; tauto.
+Qed.
+
+Lemma make_conj_impl : forall (A : Type) (eval : A -> Prop) (l : list A) (g : Prop),
+  (make_conj eval l -> g) <-> make_impl eval l g.
+Proof.
+  induction l.
+  simpl.
+  tauto.
+  simpl.
+  intros.
+  destruct l.
+  simpl.
+  tauto.
+  generalize (IHl g).
+  tauto.
+Qed.
+
+Lemma make_conj_in : forall (A : Type) (eval : A -> Prop) (l : list A),
+  make_conj eval l -> (forall p, In p l -> eval p).
+Proof.
+  induction l.
+  simpl.
+  tauto.
+  simpl.
+  intros.
+  destruct l.
+  simpl in H0.
+  destruct H0.
+  subst; auto.
+  tauto.
+  destruct H.
+  destruct H0.
+  subst;auto.
+  apply IHl; auto.
+Qed.
+
diff --git a/contrib/micromega/RingMicromega.v b/contrib/micromega/RingMicromega.v
new file mode 100644
index 000000000..2d565321a
--- /dev/null
+++ b/contrib/micromega/RingMicromega.v
@@ -0,0 +1,570 @@
+Require Import Ring_polynom.
+
+
+Require Import NArith.
+Require Import Relation_Definitions.
+Require Import Setoid.
+Require Import Ring_polynom.
+Require Import List.
+Require Import Bool.
+Require Import OrderedRing.
+Require Import Refl.
+Require Import CheckerMaker.
+
+Set Implicit Arguments.
+
+Import OrderedRingSyntax.
+
+Section Micromega.
+
+(* Assume we have a strict(ly?) ordered ring *)
+
+Variable R : Type.
+Variables rO rI : R.
+Variables rplus rtimes rminus: R -> R -> R.
+Variable ropp : R -> R.
+Variables req rle rlt : R -> R -> Prop.
+
+Variable sor : SOR rO rI rplus rtimes rminus ropp req rle rlt.
+
+Notation "0" := rO.
+Notation "1" := rI.
+Notation "x + y" := (rplus x y).
+Notation "x * y " := (rtimes x y).
+Notation "x - y " := (rminus x y).
+Notation "- x" := (ropp x).
+Notation "x == y" := (req x y).
+Notation "x ~= y" := (~ req x y).
+Notation "x <= y" := (rle x y).
+Notation "x < y" := (rlt x y).
+
+(* Assume we have a type of coefficients C and a morphism from C to R *)
+
+Variable C : Type.
+Variables cO cI : C.
+Variables cplus ctimes cminus: C -> C -> C.
+Variable copp : C -> C.
+Variables ceqb cleb : C -> C -> bool.
+Variable phi : C -> R.
+
+(* Power coefficients *)
+Variable E : Set. (* the type of exponents *)
+Variable pow_phi : N -> E.
+Variable rpow : R -> E -> R.
+
+Notation "[ x ]" := (phi x).
+Notation "x [=] y" := (ceqb x y).
+Notation "x [<=] y" := (cleb x y).
+
+(* Let's collect all hypotheses in addition to the ordered ring axioms into
+one structure *)
+
+Record SORaddon := mk_SOR_addon {
+  SORrm : ring_morph 0 1 rplus rtimes rminus ropp req cO cI cplus ctimes cminus copp ceqb phi;
+  SORpower : power_theory rI rtimes req pow_phi rpow;
+  SORcneqb_morph : forall x y : C, x [=] y = false -> [x] ~= [y];
+  SORcleb_morph : forall x y : C, x [<=] y = true -> [x] <= [y]
+}.
+
+Variable addon : SORaddon.
+
+Add Relation R req
+  reflexivity proved by sor.(SORsetoid).(Seq_refl _ _)
+  symmetry proved by sor.(SORsetoid).(Seq_sym _ _)
+  transitivity proved by sor.(SORsetoid).(Seq_trans _ _)
+as micomega_sor_setoid.
+
+Add Morphism rplus with signature req ==> req ==> req as rplus_morph.
+Proof.
+exact sor.(SORplus_wd).
+Qed.
+Add Morphism rtimes with signature req ==> req ==> req as rtimes_morph.
+Proof.
+exact sor.(SORtimes_wd).
+Qed.
+Add Morphism ropp with signature req ==> req as ropp_morph.
+Proof.
+exact sor.(SORopp_wd).
+Qed.
+Add Morphism rle with signature req ==> req ==> iff as rle_morph.
+Proof.
+exact sor.(SORle_wd).
+Qed.
+Add Morphism rlt with signature req ==> req ==> iff as rlt_morph.
+Proof.
+exact sor.(SORlt_wd).
+Qed.
+
+Add Morphism rminus with signature req ==> req ==> req as rminus_morph.
+Proof (rminus_morph sor). (* We already proved that minus is a morphism in OrderedRing.v *)
+
+Definition cneqb (x y : C) := negb (ceqb x y).
+Definition cltb (x y : C) := (cleb x y) && (cneqb x y).
+
+Notation "x [~=] y" := (cneqb x y).
+Notation "x [<] y" := (cltb x y).
+
+Ltac le_less := rewrite (Rle_lt_eq sor); left; try assumption.
+Ltac le_equal := rewrite (Rle_lt_eq sor); right; try reflexivity; try assumption.
+Ltac le_elim H := rewrite (Rle_lt_eq sor) in H; destruct H as [H | H].
+
+Lemma cleb_sound : forall x y : C, x [<=] y = true -> [x] <= [y].
+Proof addon.(SORcleb_morph).
+
+Lemma cneqb_sound : forall x y : C, x [~=] y = true -> [x] ~= [y].
+Proof.
+intros x y H1. apply addon.(SORcneqb_morph). unfold cneqb, negb in H1.
+destruct (ceqb x y); now try discriminate.
+Qed.
+
+Lemma cltb_sound : forall x y : C, x [<] y = true -> [x] < [y].
+Proof.
+intros x y H. unfold cltb in H. apply andb_prop in H. destruct H as [H1 H2].
+apply cleb_sound in H1. apply cneqb_sound in H2. apply <- (Rlt_le_neq sor). now split.
+Qed.
+
+(* Begin Micromega *)
+
+Definition PExprC := PExpr C. (* arbitrary expressions built from +, *, - *)
+Definition PolC := Pol C. (* polynomials in generalized Horner form, defined in Ring_polynom *)
+Definition Env := list R.
+
+Definition eval_pexpr : Env -> PExprC -> R := PEeval 0 rplus rtimes rminus ropp phi pow_phi rpow.
+Definition eval_pol : Env -> PolC -> R := Pphi 0 rplus rtimes phi.
+
+Inductive Op2 : Set := (* binary relations *)
+| OpEq
+| OpNEq
+| OpLe
+| OpGe
+| OpLt
+| OpGt.
+
+Definition eval_op2 (o : Op2) : R -> R -> Prop :=
+match o with
+| OpEq => req
+| OpNEq => fun x y : R => x ~= y
+| OpLe => rle
+| OpGe => fun x y : R => y <= x
+| OpLt => fun x y : R => x < y
+| OpGt => fun x y : R => y < x
+end.
+
+Record Formula : Type := {
+  Flhs : PExprC;
+  Fop : Op2;
+  Frhs : PExprC
+}.
+
+Definition eval_formula (env : Env) (f : Formula) : Prop :=
+  let (lhs, op, rhs) := f in
+    (eval_op2 op) (eval_pexpr env lhs) (eval_pexpr env rhs).
+
+(* We normalize Formulas by moving terms to one side *)
+
+Inductive Op1 : Set := (* relations with 0 *)
+| Equal (* == 0 *)
+| NonEqual (* ~= 0 *)
+| Strict (* > 0 *)
+| NonStrict (* >= 0 *).
+
+Definition NFormula := (PExprC * Op1)%type. (* normalized formula *)
+
+Definition eval_op1 (o : Op1) : R -> Prop :=
+match o with
+| Equal => fun x => x == 0
+| NonEqual => fun x : R => x ~= 0
+| Strict => fun x : R => 0 < x
+| NonStrict => fun x : R => 0 <= x
+end.
+
+Definition eval_nformula (env : Env) (f : NFormula) : Prop :=
+let (p, op) := f in eval_op1 op (eval_pexpr env p).
+
+Definition normalise (f : Formula) : NFormula :=
+let (lhs, op, rhs) := f in
+  match op with
+  | OpEq => (PEsub lhs rhs, Equal)
+  | OpNEq => (PEsub lhs rhs, NonEqual)
+  | OpLe => (PEsub rhs lhs, NonStrict)
+  | OpGe => (PEsub lhs rhs, NonStrict)
+  | OpGt => (PEsub lhs rhs, Strict)
+  | OpLt => (PEsub rhs lhs, Strict)
+  end.
+
+Definition negate (f : Formula) : NFormula :=
+let (lhs, op, rhs) := f in
+  match op with
+  | OpEq => (PEsub rhs lhs, NonEqual)
+  | OpNEq => (PEsub rhs lhs, Equal)
+  | OpLe => (PEsub lhs rhs, Strict) (* e <= e' == ~ e > e' *)
+  | OpGe => (PEsub rhs lhs, Strict)
+  | OpGt => (PEsub rhs lhs, NonStrict)
+  | OpLt => (PEsub lhs rhs, NonStrict)
+end.
+
+Theorem normalise_sound :
+  forall (env : Env) (f : Formula),
+    eval_formula env f -> eval_nformula env (normalise f).
+Proof.
+intros env f H; destruct f as [lhs op rhs]; simpl in *.
+destruct op; simpl in *.
+now apply <- (Rminus_eq_0 sor).
+intros H1. apply -> (Rminus_eq_0 sor) in H1. now apply H.
+now apply -> (Rle_le_minus sor).
+now apply -> (Rle_le_minus sor).
+now apply -> (Rlt_lt_minus sor).
+now apply -> (Rlt_lt_minus sor).
+Qed.
+
+Theorem negate_correct :
+  forall (env : Env) (f : Formula),
+    eval_formula env f <-> ~ (eval_nformula env (negate f)).
+Proof.
+intros env f; destruct f as [lhs op rhs]; simpl.
+destruct op; simpl.
+symmetry. rewrite (Rminus_eq_0 sor).
+split; intro H; [symmetry; now apply -> (Req_dne sor) | symmetry in H; now apply <- (Req_dne sor)].
+rewrite (Rminus_eq_0 sor). split; intro; now apply (Rneq_symm sor).
+rewrite <- (Rlt_lt_minus sor). now rewrite <- (Rle_ngt sor).
+rewrite <- (Rlt_lt_minus sor). now rewrite <- (Rle_ngt sor).
+rewrite <- (Rle_le_minus sor). now rewrite <- (Rlt_nge sor).
+rewrite <- (Rle_le_minus sor). now rewrite <- (Rlt_nge sor).
+Qed.
+
+Definition OpMult (o o' : Op1) : Op1 :=
+match o with
+| Equal => Equal
+| NonStrict => NonStrict (* (OpMult NonStrict Equal) could be defined as Equal *)
+| Strict => o'
+| NonEqual => NonEqual (* does not matter what we return here; see the following lemmas *)
+end.
+
+Definition OpAdd (o o': Op1) : Op1 :=
+match o with
+| Equal => o'
+| NonStrict =>
+  match o' with
+  | Strict => Strict
+  | _ => NonStrict
+  end
+| Strict => Strict
+| NonEqual => NonEqual (* does not matter what we return here *)
+end.
+
+Lemma OpMultNonEqual :
+  forall o o' : Op1, o <> NonEqual -> o' <> NonEqual -> OpMult o o' <> NonEqual.
+Proof.
+intros o o' H1 H2; destruct o; destruct o'; simpl; try discriminate;
+try (intro H; apply H1; reflexivity);
+try (intro H; apply H2; reflexivity).
+Qed.
+
+Lemma OpAdd_NonEqual :
+  forall o o' : Op1, o <> NonEqual -> o' <> NonEqual -> OpAdd o o' <> NonEqual.
+Proof.
+intros o o' H1 H2; destruct o; destruct o'; simpl; try discriminate;
+try (intro H; apply H1; reflexivity);
+try (intro H; apply H2; reflexivity).
+Qed.
+
+Lemma OpMult_sound :
+  forall (o o' : Op1) (x y : R), o <> NonEqual -> o' <> NonEqual ->
+    eval_op1 o x -> eval_op1 o' y -> eval_op1 (OpMult o o') (x * y).
+Proof.
+unfold eval_op1; destruct o; simpl; intros o' x y H1 H2 H3 H4.
+rewrite H3; now rewrite (Rtimes_0_l sor).
+elimtype False; now apply H1.
+destruct o'.
+rewrite H4; now rewrite (Rtimes_0_r sor).
+elimtype False; now apply H2.
+now apply (Rtimes_pos_pos sor).
+apply (Rtimes_nonneg_nonneg sor); [le_less | assumption].
+destruct o'.
+rewrite H4, (Rtimes_0_r sor); le_equal.
+elimtype False; now apply H2.
+apply (Rtimes_nonneg_nonneg sor); [assumption | le_less].
+now apply (Rtimes_nonneg_nonneg sor).
+Qed.
+
+Lemma OpAdd_sound :
+  forall (o o' : Op1) (e e' : R), o <> NonEqual -> o' <> NonEqual ->
+    eval_op1 o e -> eval_op1 o' e' -> eval_op1 (OpAdd o o') (e + e').
+Proof.
+unfold eval_op1; destruct o; simpl; intros o' e e' H1 H2 H3 H4.
+destruct o'.
+now rewrite H3, H4, (Rplus_0_l sor).
+elimtype False; now apply H2.
+now rewrite H3, (Rplus_0_l sor).
+now rewrite H3, (Rplus_0_l sor).
+elimtype False; now apply H1.
+destruct o'.
+now rewrite H4, (Rplus_0_r sor).
+elimtype False; now apply H2.
+now apply (Rplus_pos_pos sor).
+now apply (Rplus_pos_nonneg sor).
+destruct o'.
+now rewrite H4, (Rplus_0_r sor).
+elimtype False; now apply H2.
+now apply (Rplus_nonneg_pos sor).
+now apply (Rplus_nonneg_nonneg sor).
+Qed.
+
+(* We consider a monoid whose generators are polynomials from the
+hypotheses of the form (p ~= 0). Thus it follows from the hypotheses that
+every element of the monoid (i.e., arbitrary product of generators) is ~=
+0. Therefore, the square of every element is > 0. *)
+
+Inductive Monoid (l : list NFormula) : PExprC -> Prop :=
+| M_One : Monoid l (PEc cI)
+| M_In : forall p : PExprC, In (p, NonEqual) l -> Monoid l p
+| M_Mult : forall (e1 e2 : PExprC), Monoid l e1 -> Monoid l e2 -> Monoid l (PEmul e1 e2).
+
+Inductive Cone (l : list (NFormula)) : PExprC -> Op1 -> Prop :=
+| InC : forall p op, In (p, op) l -> op <> NonEqual -> Cone l p op
+| IsIdeal : forall p, Cone l p Equal -> forall p', Cone l (PEmul p p') Equal
+| IsSquare : forall p, Cone l (PEmul p p) NonStrict
+| IsMonoid : forall p, Monoid l p -> Cone l (PEmul p p) Strict
+| IsMult : forall p op q oq, Cone l p op -> Cone l q oq -> Cone l (PEmul p q) (OpMult op oq)
+| IsAdd : forall p op q oq, Cone l p op -> Cone l q oq -> Cone l (PEadd p q) (OpAdd op oq)
+| IsPos : forall c : C, cltb cO c = true -> Cone l (PEc c) Strict
+| IsZ : Cone l (PEc cO) Equal.
+
+(* As promised, if all hypotheses are true in some environment, then every
+member of the monoid is nonzero in this environment *)
+
+Lemma monoid_nonzero : forall (l : list NFormula) (env : Env),
+  (forall f : NFormula, In f l -> eval_nformula env f) ->
+    forall p : PExprC, Monoid l p -> eval_pexpr env p ~= 0.
+Proof.
+intros l env H1 p H2. induction H2 as [| f H | e1 e2 H3 IH1 H4 IH2]; simpl.
+rewrite addon.(SORrm).(morph1). apply (Rneq_symm sor). apply (Rneq_0_1 sor).
+apply H1 in H. now simpl in H.
+simpl in IH1, IH2. apply (Rtimes_neq_0 sor). now split.
+Qed.
+
+(* If all members of a cone base are true in some environment, then every
+member of the cone is true as well *)
+
+Lemma cone_true :
+  forall (l : list NFormula) (env : Env),
+    (forall (f : NFormula), In f l -> eval_nformula env f) ->
+      forall (p : PExprC) (op : Op1), Cone l p op ->
+        op <> NonEqual /\ eval_nformula env (p, op).
+Proof.
+intros l env H1 p op H2. induction H2; simpl in *.
+split. assumption. apply H1 in H. now unfold eval_nformula in H.
+split. discriminate. destruct IHCone as [_ H3]. rewrite H3. now rewrite (Rtimes_0_l sor).
+split. discriminate. apply (Rtimes_square_nonneg sor).
+split. discriminate. apply <- (Rlt_le_neq sor). split. apply (Rtimes_square_nonneg sor).
+apply (Rneq_symm sor). apply (Rtimes_neq_0 sor). split; now apply monoid_nonzero with l.
+destruct IHCone1 as [IH1 IH2]; destruct IHCone2 as [IH3 IH4].
+split. now apply OpMultNonEqual. now apply OpMult_sound.
+destruct IHCone1 as [IH1 IH2]; destruct IHCone2 as [IH3 IH4].
+split. now apply OpAdd_NonEqual. now apply OpAdd_sound.
+split. discriminate. rewrite <- addon.(SORrm).(morph0). now apply cltb_sound.
+split. discriminate. apply addon.(SORrm).(morph0).
+Qed.
+
+(* Every element of a monoid is a product of some generators; therefore,
+to determine an element we can give a list of generators' indices *)
+
+Definition MonoidMember : Set := list nat.
+
+Inductive ConeMember : Type :=
+| S_In : nat -> ConeMember
+| S_Ideal : PExprC -> ConeMember -> ConeMember
+| S_Square : PExprC -> ConeMember
+| S_Monoid : MonoidMember -> ConeMember
+| S_Mult : ConeMember -> ConeMember -> ConeMember
+| S_Add : ConeMember -> ConeMember -> ConeMember
+| S_Pos : forall c : C, cltb cO c = true -> ConeMember (* the proof of cltb 0 c = true should be (refl_equal true) *)
+| S_Z : ConeMember.
+
+Definition nformula_times (f f' : NFormula) : NFormula :=
+let (p, op) := f in
+  let (p', op') := f' in
+    (PEmul p p', OpMult op op').
+
+Definition nformula_plus (f f' : NFormula) : NFormula :=
+let (p, op) := f in
+  let (p', op') := f' in
+    (PEadd p p', OpAdd op op').
+
+Definition nformula_times_0 (p : PExprC) (f : NFormula) : NFormula :=
+let (q, op) := f in
+  match op with
+  | Equal => (PEmul q p, Equal)
+  | _ => f
+  end.
+
+Fixpoint eval_monoid (l : list NFormula) (ns : MonoidMember) {struct ns} : PExprC :=
+match ns with
+| nil => PEc cI
+| n :: ns =>
+  let p := match nth n l (PEc cI, NonEqual) with
+           | (q, NonEqual) => q
+           | _ => PEc cI
+           end in
+    PEmul p (eval_monoid l ns)
+end.
+
+Theorem eval_monoid_in_monoid :
+  forall (l : list NFormula) (ns : MonoidMember), Monoid l (eval_monoid l ns).
+Proof.
+intro l; induction ns; simpl in *.
+constructor.
+apply M_Mult; [| assumption].
+destruct (nth_in_or_default a l (PEc cI, NonEqual)).
+destruct (nth a l (PEc cI, NonEqual)). destruct o; try constructor. assumption.
+rewrite e; simpl. constructor.
+Qed.
+
+(* Provides the cone member from the witness, i.e., ConeMember *)
+Fixpoint eval_cone (l : list NFormula) (cm : ConeMember) {struct cm} : NFormula :=
+match cm with
+| S_In n => match nth n l (PEc cO, Equal) with
+            | (_, NonEqual) => (PEc cO, Equal)
+            | f => f
+            end
+| S_Ideal p cm' => nformula_times_0 p (eval_cone l cm')
+| S_Square p => (PEmul p p, NonStrict)
+| S_Monoid m => let p := eval_monoid l m in (PEmul p p, Strict)
+| S_Mult p q => nformula_times (eval_cone l p) (eval_cone l q)
+| S_Add p q => nformula_plus (eval_cone l p) (eval_cone l q)
+| S_Pos c _ => (PEc c, Strict)
+| S_Z => (PEc cO, Equal)
+end.
+
+Theorem eval_cone_in_cone :
+  forall (l : list NFormula) (cm : ConeMember),
+    let (p, op) := eval_cone l cm in Cone l p op.
+Proof.
+intros l cm; induction cm; simpl.
+destruct (nth_in_or_default n l (PEc cO, Equal)).
+destruct (nth n l (PEc cO, Equal)). destruct o; try (now apply InC). apply IsZ.
+rewrite e. apply IsZ.
+destruct (eval_cone l cm). destruct o; simpl; try assumption. now apply IsIdeal.
+apply IsSquare.
+apply IsMonoid. apply eval_monoid_in_monoid.
+destruct (eval_cone l cm1). destruct (eval_cone l cm2). unfold nformula_times. now apply IsMult.
+destruct (eval_cone l cm1). destruct (eval_cone l cm2). unfold nformula_plus. now apply IsAdd.
+now apply IsPos. apply IsZ.
+Qed.
+
+(* (inconsistent_cone_member l p) means (p, op) is in the cone for some op
+(> 0, >= 0, == 0, or ~= 0) and this formula is inconsistent. This fact
+implies that l is inconsistent, as shown by the next lemma. Inconsistency
+of a formula (p, op) can be established by normalizing p and showing that
+it is a constant c for which (c, op) is false. (This is only a sufficient,
+not necessary, condition, of course.) Membership in the cone can be
+verified if we have a certificate. *)
+
+Definition inconsistent_cone_member (l : list NFormula) (p : PExprC) :=
+  exists op : Op1, Cone l p op /\
+    forall env : Env, ~ eval_op1 op (eval_pexpr env p).
+
+Implicit Arguments make_impl [A].
+
+(* If some element of a cone is inconsistent, then the base of the cone
+is also inconsistent *)
+
+Lemma prove_inconsistent :
+  forall (l : list NFormula) (p : PExprC),
+    inconsistent_cone_member l p -> forall env, make_impl (eval_nformula env) l False.
+Proof.
+intros l p H env.
+destruct H as [o [wit H]].
+apply -> make_conj_impl.
+intro H1. apply H with env.
+pose proof (@cone_true l env) as H2.
+cut (forall f : NFormula, In f l -> eval_nformula env f). intro H3.
+apply (proj2 (H2 H3 p o wit)). intro. now apply make_conj_in.
+Qed.
+
+Definition normalise_pexpr : PExprC -> PolC :=
+  norm_aux cO cI cplus ctimes cminus copp ceqb.
+
+Let Reqe := mk_reqe rplus rtimes ropp req
+  sor.(SORplus_wd)
+  sor.(SORtimes_wd)
+  sor.(SORopp_wd).
+
+Theorem normalise_pexpr_correct :
+  forall (env : Env) (e : PExprC), eval_pexpr env e == eval_pol env (normalise_pexpr e).
+intros env e. unfold eval_pexpr, eval_pol, normalise_pexpr.
+apply (norm_aux_spec sor.(SORsetoid) Reqe (Rth_ARth sor.(SORsetoid) Reqe sor.(SORrt))
+addon.(SORrm) addon.(SORpower) nil). constructor.
+Qed.
+
+(* Check that a formula f is inconsistent by normalizing and comparing the
+resulting constant with 0 *)
+
+Definition check_inconsistent (f : NFormula) : bool :=
+let (e, op) := f in
+  match normalise_pexpr e with
+  | Pc c =>
+    match op with
+    | Equal => cneqb c cO
+    | NonStrict => c [<] cO
+    | Strict => c [<=] cO
+    | NonEqual => false (* eval_cone never returns (p, NonEqual) *)
+    end
+  | _ => false (* not a constant *)
+  end.
+
+Lemma check_inconsistent_sound :
+  forall (p : PExprC) (op : Op1),
+    check_inconsistent (p, op) = true -> forall env, ~ eval_op1 op (eval_pexpr env p).
+Proof.
+intros p op H1 env. unfold check_inconsistent in H1.
+destruct op; simpl; rewrite normalise_pexpr_correct;
+destruct (normalise_pexpr p); simpl; try discriminate H1;
+rewrite <- addon.(SORrm).(morph0).
+now apply cneqb_sound.
+apply cleb_sound in H1. now apply -> (Rle_ngt sor).
+apply cltb_sound in H1. now apply -> (Rlt_nge sor).
+Qed.
+
+Definition check_normalised_formulas : list NFormula -> ConeMember -> bool :=
+  fun l cm => check_inconsistent (eval_cone l cm).
+
+Lemma checker_nf_sound :
+  forall (l : list NFormula) (cm : ConeMember),
+    check_normalised_formulas l cm = true ->
+      forall env : Env, make_impl (eval_nformula env) l False.
+Proof.
+intros l cm H env.
+unfold check_normalised_formulas in H.
+case_eq (eval_cone l cm). intros p op H1.
+apply prove_inconsistent with p. unfold inconsistent_cone_member. exists op. split.
+pose proof (eval_cone_in_cone l cm) as H2. now rewrite H1 in H2.
+apply check_inconsistent_sound. now rewrite <- H1.
+Qed.
+
+Definition check_formulas :=
+  CheckerMaker.check_formulas normalise check_normalised_formulas.
+
+Theorem check_formulas_sound :
+  forall (l : list Formula) (w : ConeMember),
+    check_formulas l w = true ->
+      forall env : Env, make_impl (eval_formula env) l False.
+Proof.
+exact (CheckerMaker.check_formulas_sound eval_formula eval_nformula normalise
+       normalise_sound check_normalised_formulas checker_nf_sound).
+Qed.
+
+Definition check_conj_formulas :=
+  CheckerMaker.check_conj_formulas normalise negate check_normalised_formulas.
+
+Theorem check_conj_formulas_sound :
+  forall (l1 : list Formula) (l2 : list Formula) (ws : list ConeMember),
+    check_conj_formulas l1 ws l2 = true ->
+      forall env : Env, make_impl (eval_formula env) l1 (make_conj (eval_formula env) l2).
+Proof.
+exact (check_conj_formulas_sound eval_formula eval_nformula normalise negate
+       normalise_sound negate_correct check_normalised_formulas checker_nf_sound).
+Qed.
+
+End Micromega.
+
diff --git a/contrib/micromega/ZCoeff.v b/contrib/micromega/ZCoeff.v
new file mode 100644
index 000000000..20c900780
--- /dev/null
+++ b/contrib/micromega/ZCoeff.v
@@ -0,0 +1,142 @@
+Require Import OrderedRing.
+Require Import RingMicromega.
+Require Import ZArith.
+Require Import InitialRing.
+Require Import Setoid.
+
+Import OrderedRingSyntax.
+
+Set Implicit Arguments.
+
+Section InitialMorphism.
+
+Variable R : Type.
+Variables rO rI : R.
+Variables rplus rtimes rminus: R -> R -> R.
+Variable ropp : R -> R.
+Variables req rle rlt : R -> R -> Prop.
+
+Variable sor : SOR rO rI rplus rtimes rminus ropp req rle rlt.
+
+Notation "0" := rO.
+Notation "1" := rI.
+Notation "x + y" := (rplus x y).
+Notation "x * y " := (rtimes x y).
+Notation "x - y " := (rminus x y).
+Notation "- x" := (ropp x).
+Notation "x == y" := (req x y).
+Notation "x ~= y" := (~ req x y).
+Notation "x <= y" := (rle x y).
+Notation "x < y" := (rlt x y).
+
+Add Relation R req
+  reflexivity proved by sor.(SORsetoid).(Seq_refl _ _)
+  symmetry proved by sor.(SORsetoid).(Seq_sym _ _)
+  transitivity proved by sor.(SORsetoid).(Seq_trans _ _)
+as sor_setoid.
+
+Add Morphism rplus with signature req ==> req ==> req as rplus_morph.
+Proof.
+exact sor.(SORplus_wd).
+Qed.
+Add Morphism rtimes with signature req ==> req ==> req as rtimes_morph.
+Proof.
+exact sor.(SORtimes_wd).
+Qed.
+Add Morphism ropp with signature req ==> req as ropp_morph.
+Proof.
+exact sor.(SORopp_wd).
+Qed.
+Add Morphism rle with signature req ==> req ==> iff as rle_morph.
+Proof.
+exact sor.(SORle_wd).
+Qed.
+Add Morphism rlt with signature req ==> req ==> iff as rlt_morph.
+Proof.
+exact sor.(SORlt_wd).
+Qed.
+Add Morphism rminus with signature req ==> req ==> req as rminus_morph.
+Proof (rminus_morph sor).
+
+Ltac le_less := rewrite (Rle_lt_eq sor); left; try assumption.
+Ltac le_equal := rewrite (Rle_lt_eq sor); right; try reflexivity; try assumption.
+
+Definition gen_order_phi_Z : Z -> R := gen_phiZ 0 1 rplus rtimes ropp.
+
+Notation phi_pos := (gen_phiPOS 1 rplus rtimes).
+Notation phi_pos1 := (gen_phiPOS1 1 rplus rtimes).
+
+Notation "[ x ]" := (gen_order_phi_Z x).
+
+Lemma ring_ops_wd : ring_eq_ext rplus rtimes ropp req.
+Proof.
+constructor.
+exact rplus_morph.
+exact rtimes_morph.
+exact ropp_morph.
+Qed.
+
+Lemma Zring_morph :
+  ring_morph 0 1 rplus rtimes rminus ropp req
+             0%Z 1%Z Zplus Zmult Zminus Zopp
+             Zeq_bool gen_order_phi_Z.
+Proof.
+exact (gen_phiZ_morph sor.(SORsetoid) ring_ops_wd sor.(SORrt)).
+Qed.
+
+Lemma phi_pos1_pos : forall x : positive, 0 < phi_pos1 x.
+Proof.
+induction x as [x IH | x IH |]; simpl;
+try apply (Rplus_pos_pos sor); try apply (Rtimes_pos_pos sor); try apply (Rplus_pos_pos sor);
+try apply (Rlt_0_1 sor); assumption.
+Qed.
+
+Lemma phi_pos1_succ : forall x : positive, phi_pos1 (Psucc x) == 1 + phi_pos1 x.
+Proof.
+exact (ARgen_phiPOS_Psucc sor.(SORsetoid) ring_ops_wd
+        (Rth_ARth sor.(SORsetoid) ring_ops_wd sor.(SORrt))).
+Qed.
+
+Lemma clt_pos_morph : forall x y : positive, (x < y)%positive -> phi_pos1 x < phi_pos1 y.
+Proof.
+intros x y H. pattern y; apply Plt_ind with x.
+rewrite phi_pos1_succ; apply (Rlt_succ_r sor).
+clear y H; intros y _ H. rewrite phi_pos1_succ. now apply (Rlt_lt_succ sor).
+assumption.
+Qed.
+
+Lemma clt_morph : forall x y : Z, (x < y)%Z -> [x] < [y].
+Proof.
+unfold Zlt; intros x y H;
+do 2 rewrite (same_genZ sor.(SORsetoid) ring_ops_wd sor.(SORrt));
+destruct x; destruct y; simpl in *; try discriminate.
+apply phi_pos1_pos.
+now apply clt_pos_morph.
+apply <- (Ropp_neg_pos sor); apply phi_pos1_pos.
+apply (Rlt_trans sor) with 0. apply <- (Ropp_neg_pos sor); apply phi_pos1_pos.
+apply phi_pos1_pos.
+rewrite Pcompare_antisym in H; simpl in H. apply -> (Ropp_lt_mono sor).
+now apply clt_pos_morph.
+Qed.
+
+Lemma Zcleb_morph : forall x y : Z, Zle_bool x y = true -> [x] <= [y].
+Proof.
+unfold Zle_bool; intros x y H.
+case_eq (x ?= y)%Z; intro H1; rewrite H1 in H.
+le_equal. apply Zring_morph.(morph_eq). unfold Zeq_bool; now rewrite H1.
+le_less. now apply clt_morph.
+discriminate.
+Qed.
+
+Lemma Zcneqb_morph : forall x y : Z, Zeq_bool x y = false -> [x] ~= [y].
+Proof.
+intros x y H. unfold Zeq_bool in H.
+case_eq (Zcompare x y); intro H1; rewrite H1 in *; (discriminate || clear H).
+apply (Rlt_neq sor). now apply clt_morph.
+fold (x > y)%Z in H1. rewrite Zgt_iff_lt in H1.
+apply (Rneq_symm sor). apply (Rlt_neq sor). now apply clt_morph.
+Qed.
+
+End InitialMorphism.
+
+
diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v
index fafc3285b..d7486bc2b 100644
--- a/theories/NArith/BinPos.v
+++ b/theories/NArith/BinPos.v
@@ -965,6 +965,11 @@ Proof.
   rewrite H; apply Pcompare_p_Sp.
 Qed.
 
+Lemma Plt_lt_succ : forall n m : positive, n < m -> n < Psucc m.
+Proof.
+unfold Plt; intros n m H; apply <- Pcompare_p_Sq; now left.
+Qed.
+
 (** 1 is the least positive number *)
 
 Lemma Pcompare_1 : forall p, ~ (p ?= xH) Eq = Lt.
@@ -972,6 +977,31 @@ Proof.
   destruct p; discriminate.
 Qed.
 
+Lemma Plt_irrefl : forall p : positive, ~ p < p.
+Proof.
+intro p; unfold Plt; rewrite Pcompare_refl; discriminate.
+Qed.
+
+Lemma Plt_trans : forall n m p : positive, n < m -> m < p -> n < p.
+Proof.
+intros n m p; unfold Plt; elim p using Pind.
+intros _ H; false_hyp H Pcompare_1.
+clear p; intros p IH H1 H2. apply -> Pcompare_p_Sq in H2.
+apply Plt_lt_succ. destruct H2 as [H2 | H2].
+now apply IH. now rewrite H2 in H1.
+Qed.
+
+Theorem Plt_ind : forall (A : positive -> Prop) (n : positive),
+  A (Psucc n) ->
+    (forall m : positive, n < m -> A m -> A (Psucc m)) ->
+      forall m : positive, n < m -> A m.
+Proof.
+intros A n AB AS m. elim m using Pind; unfold Plt.
+intro H; false_hyp H Pcompare_1.
+clear m; intros m H1 H2. apply -> Pcompare_p_Sq in H2. destruct H2 as [H2 | H2].
+auto. now rewrite <- H2.
+Qed.
+
 (**********************************************************************)
 (** Properties of subtraction on binary positive numbers *)
 
diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index ab863eb1f..bde3d9a92 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -10,7 +10,7 @@ Open Local Scope NatIntScope.
 Notation Z := NZ (only parsing).
 Notation E := NZE (only parsing).
 
-Parameter Inline Zopp : Z -> Z.
+Parameter Zopp : Z -> Z.
 
 Add Morphism Zopp with signature E ==> E as Zopp_wd.
 
diff --git a/theories/Numbers/Integer/Abstract/ZOrder.v b/theories/Numbers/Integer/Abstract/ZOrder.v
index 295f5355a..e0ef2f15d 100644
--- a/theories/Numbers/Integer/Abstract/ZOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZOrder.v
@@ -23,6 +23,9 @@ Proof NZlt_le_incl.
 Theorem Zlt_neq : forall n m : Z, n < m -> n ~= m.
 Proof NZlt_neq.
 
+Theorem Zlt_le_neq : forall n m : Z, n < m <-> n <= m /\ n ~= m.
+Proof NZlt_le_neq.
+
 Theorem Zle_refl : forall n : Z, n <= n.
 Proof NZle_refl.
 
diff --git a/theories/Numbers/Integer/Abstract/ZPlusOrder.v b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
index bab1bb4a0..6a13aa3db 100644
--- a/theories/Numbers/Integer/Abstract/ZPlusOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
@@ -30,14 +30,32 @@ Proof NZplus_lt_le_mono.
 Theorem Zplus_le_lt_mono : forall n m p q : Z, n <= m -> p < q -> n + p < m + q.
 Proof NZplus_le_lt_mono.
 
+Theorem Zplus_pos_pos : forall n m : Z, 0 < n -> 0 < m -> 0 < n + m.
+Proof NZplus_pos_pos.
+
+Theorem Zplus_pos_nonneg : forall n m : Z, 0 < n -> 0 <= m -> 0 < n + m.
+Proof NZplus_pos_nonneg.
+
+Theorem Zplus_nonneg_pos : forall n m : Z, 0 <= n -> 0 < m -> 0 < n + m.
+Proof NZplus_nonneg_pos.
+
+Theorem Zplus_nonneg_nonneg : forall n m : Z, 0 <= n -> 0 <= m -> 0 <= n + m.
+Proof NZplus_nonneg_nonneg.
+
+Theorem Zlt_plus_pos_l : forall n m : Z, 0 < n -> m < n + m.
+Proof NZlt_plus_pos_l.
+
+Theorem Zlt_plus_pos_r : forall n m : Z, 0 < n -> m < m + n.
+Proof NZlt_plus_pos_r.
+
 Theorem Zle_lt_plus_lt : forall n m p q : Z, n <= m -> p + m < q + n -> p < q.
 Proof NZle_lt_plus_lt.
 
 Theorem Zlt_le_plus_lt : forall n m p q : Z, n < m -> p + m <= q + n -> p < q.
 Proof NZlt_le_plus_lt.
 
-Theorem Zle_le_plus_lt : forall n m p q : Z, n <= m -> p + m <= q + n -> p <= q.
-Proof NZle_le_plus_lt.
+Theorem Zle_le_plus_le : forall n m p q : Z, n <= m -> p + m <= q + n -> p <= q.
+Proof NZle_le_plus_le.
 
 Theorem Zplus_lt_cases : forall n m p q : Z, n + m < p + q -> n < p \/ m < q.
 Proof NZplus_lt_cases.
@@ -57,89 +75,6 @@ Proof NZplus_nonpos_cases.
 Theorem Zplus_nonneg_cases : forall n m : Z, 0 <= n + m -> 0 <= n \/ 0 <= m.
 Proof NZplus_nonneg_cases.
 
-(** Multiplication and order *)
-
-Theorem Ztimes_lt_pred :
-  forall p q n m : Z, S p == q -> (p * n < p * m <-> q * n + m < q * m + n).
-Proof NZtimes_lt_pred.
-
-Theorem Ztimes_lt_mono_pos_l : forall p n m : Z, 0 < p -> (n < m <-> p * n < p * m).
-Proof NZtimes_lt_mono_pos_l.
-
-Theorem Ztimes_lt_mono_pos_r : forall p n m : Z, 0 < p -> (n < m <-> n * p < m * p).
-Proof NZtimes_lt_mono_pos_r.
-
-Theorem Ztimes_lt_mono_neg_l : forall p n m : Z, p < 0 -> (n < m <-> p * m < p * n).
-Proof NZtimes_lt_mono_neg_l.
-
-Theorem Ztimes_lt_mono_neg_r : forall p n m : Z, p < 0 -> (n < m <-> m * p < n * p).
-Proof NZtimes_lt_mono_neg_r.
-
-Theorem Ztimes_le_mono_nonneg_l : forall n m p : Z, 0 <= p -> n <= m -> p * n <= p * m.
-Proof NZtimes_le_mono_nonneg_l.
-
-Theorem Ztimes_le_mono_nonpos_l : forall n m p : Z, p <= 0 -> n <= m -> p * m <= p * n.
-Proof NZtimes_le_mono_nonpos_l.
-
-Theorem Ztimes_le_mono_nonneg_r : forall n m p : Z, 0 <= p -> n <= m -> n * p <= m * p.
-Proof NZtimes_le_mono_nonneg_r.
-
-Theorem Ztimes_le_mono_nonpos_r : forall n m p : Z, p <= 0 -> n <= m -> m * p <= n * p.
-Proof NZtimes_le_mono_nonpos_r.
-
-Theorem Ztimes_cancel_l : forall n m p : Z, p ~= 0 -> (p * n == p * m <-> n == m).
-Proof NZtimes_cancel_l.
-
-Theorem Ztimes_le_mono_pos_l : forall n m p : Z, 0 < p -> (n <= m <-> p * n <= p * m).
-Proof NZtimes_le_mono_pos_l.
-
-Theorem Ztimes_le_mono_pos_r : forall n m p : Z, 0 < p -> (n <= m <-> n * p <= m * p).
-Proof NZtimes_le_mono_pos_r.
-
-Theorem Ztimes_le_mono_neg_l : forall n m p : Z, p < 0 -> (n <= m <-> p * m <= p * n).
-Proof NZtimes_le_mono_neg_l.
-
-Theorem Ztimes_le_mono_neg_r : forall n m p : Z, p < 0 -> (n <= m <-> m * p <= n * p).
-Proof NZtimes_le_mono_neg_r.
-
-Theorem Ztimes_lt_mono :
-  forall n m p q : Z, 0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q.
-Proof NZtimes_lt_mono.
-
-Theorem Ztimes_le_mono :
-  forall n m p q : Z, 0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q.
-Proof NZtimes_le_mono.
-
-Theorem Ztimes_pos_pos : forall n m : Z, 0 < n -> 0 < m -> 0 < n * m.
-Proof NZtimes_pos_pos.
-
-Theorem Ztimes_nonneg_nonneg : forall n m : Z, 0 <= n -> 0 <= m -> 0 <= n * m.
-Proof NZtimes_nonneg_nonneg.
-
-Theorem Ztimes_neg_neg : forall n m : Z, n < 0 -> m < 0 -> 0 < n * m.
-Proof NZtimes_neg_neg.
-
-Theorem Ztimes_nonpos_nonpos : forall n m : Z, n <= 0 -> m <= 0 -> 0 <= n * m.
-Proof NZtimes_nonpos_nonpos.
-
-Theorem Ztimes_pos_neg : forall n m : Z, 0 < n -> m < 0 -> n * m < 0.
-Proof NZtimes_pos_neg.
-
-Theorem Ztimes_nonneg_nonpos : forall n m : Z, 0 <= n -> m <= 0 -> n * m <= 0.
-Proof NZtimes_nonneg_nonpos.
-
-Theorem Ztimes_neg_pos : forall n m : Z, n < 0 -> 0 < m -> n * m < 0.
-Proof NZtimes_neg_pos.
-
-Theorem Ztimes_nonpos_nonneg : forall n m : Z, n <= 0 -> 0 <= m -> n * m <= 0.
-Proof NZtimes_nonpos_nonneg.
-
-Theorem Ztimes_eq_0 : forall n m : Z, n * m == 0 -> n == 0 \/ m == 0.
-Proof NZtimes_eq_0.
-
-Theorem Ztimes_neq_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
-Proof NZtimes_neq_0.
-
 (** Theorems that are either not valid on N or have different proofs on N and Z *)
 
 (** Minus and order *)
@@ -252,7 +187,7 @@ Qed.
 
 Theorem Zle_le_minus_lt : forall n m p q : Z, n <= m -> p - n <= q - m -> p <= q.
 Proof.
-intros n m p q H1 H2. apply (Zle_le_plus_lt (- m) (- n));
+intros n m p q H1 H2. apply (Zle_le_plus_le (- m) (- n));
 [now apply -> Zopp_le_mono | now do 2 rewrite Zplus_opp_minus].
 Qed.
 
diff --git a/theories/Numbers/Integer/Abstract/ZTimesOrder.v b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
index d63dc0d8c..438142095 100644
--- a/theories/Numbers/Integer/Abstract/ZTimesOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
@@ -94,6 +94,9 @@ Theorem Ztimes_neg :
   forall n m : Z, n * m < 0 <-> (n < 0 /\ m > 0) \/ (n > 0 /\ m < 0).
 Proof NZtimes_neg.
 
+Theorem Ztimes_2_mono_l : forall n m : Z, n < m -> 1 + (1 + 1) * n < (1 + 1) * m.
+Proof NZtimes_2_mono_l.
+
 (** Theorems that are either not valid on N or have different proofs on N and Z *)
 
 (* None? *)
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index cb8ac3b5b..0a52d214a 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -132,7 +132,14 @@ Qed.
 
 End NZOrdAxiomsMod.
 
-Definition Zopp := Zopp.
+Definition Zopp (x : Z) :=
+match x with
+| Z0 => Z0
+| Zpos x => Zneg x
+| Zneg x => Zpos x
+end.
+
+Notation "- x" := (Zopp x) : Z_scope.
 
 Add Morphism Zopp with signature NZE ==> NZE as Zopp_wd.
 Proof.
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 5c8b5890d..9a012b26c 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -1,48 +1,82 @@
 Require Import NMinus. (* The most complete file for natural numbers *)
-Require Import ZTimesOrder. (* The most complete file for integers *)
+Require Export ZTimesOrder. (* The most complete file for integers *)
 
 Module ZPairsAxiomsMod (Import NAxiomsMod : NAxiomsSig) <: ZAxiomsSig.
 Module Import NPropMod := NMinusPropFunct NAxiomsMod. (* Get all properties of natural numbers *)
-Notation Local N := NZ. (* To remember N without having to use a long qualifying name *)
-Notation Local NE := NZE (only parsing).
-Notation Local plus_wd := NZplus_wd (only parsing).
+
+(* The definitios of functions (NZplus, NZtimes, etc.) will be unfolded by
+the properties functor. Since we don't want Zplus_comm to refer to unfolded
+definitions of equality: fun p1 p2 : NZ => (fst p1 + snd p2) = (fst p2 + snd p1),
+we will provide an extra layer of definitions. *)
+
 Open Local Scope NatIntScope.
+Definition Z := (N * N)%type.
+Definition Z0 : Z := (0, 0).
+Definition Zeq (p1 p2 : Z) := ((fst p1) + (snd p2) == (fst p2) + (snd p1)).
+Definition Zsucc (n : Z) : Z := (S (fst n), snd n).
+Definition Zpred (n : Z) : Z := (fst n, S (snd n)).
 
-Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
-Module Export NZAxiomsMod <: NZAxiomsSig.
+(* We do not have Zpred (Zsucc n) = n but only Zpred (Zsucc n) = n. It
+could be possible to consider as canonical only pairs where one of the
+elements is 0, and make all operations convert canonical values into other
+canonical values. In that case, we could get rid of setoids as well as
+arrive at integers as signed natural numbers. *)
+
+Definition Zplus (n m : Z) : Z := ((fst n) + (fst m), (snd n) + (snd m)).
+Definition Zminus (n m : Z) : Z := ((fst n) + (snd m), (snd n) + (fst m)).
 
-Definition NZ : Set := (NZ * NZ)%type.
-Definition NZE (p1 p2 : NZ) := ((fst p1) + (snd p2) == (fst p2) + (snd p1)).
-Notation Z := NZ (only parsing).
-Notation E := NZE (only parsing).
-Definition NZ0 := (0, 0).
-Definition NZsucc (n : Z) := (S (fst n), snd n).
-Definition NZpred (n : Z) := (fst n, S (snd n)).
-(* We do not have P (S n) = n but only P (S n) == n. It could be possible
-to consider as canonical only pairs where one of the elements is 0, and
-make all operations convert canonical values into other canonical values.
-In that case, we could get rid of setoids as well as arrive at integers as
-signed natural numbers. *)
-Definition NZplus (n m : Z) := ((fst n) + (fst m), (snd n) + (snd m)).
-Definition NZminus (n m : Z) := ((fst n) + (snd m), (snd n) + (fst m)).
 (* Unfortunately, the elements of the pair keep increasing, even during
 subtraction *)
-Definition NZtimes (n m : Z) :=
+
+Definition Ztimes (n m : Z) : Z :=
   ((fst n) * (fst m) + (snd n) * (snd m), (fst n) * (snd m) + (snd n) * (fst m)).
+Definition Zlt (n m : Z) := (fst n) + (snd m) < (fst m) + (snd n).
+Definition Zle (n m : Z) := (fst n) + (snd m) <= (fst m) + (snd n).
 
-Theorem ZE_refl : reflexive Z E.
+Delimit Scope IntScope with Int.
+Bind Scope IntScope with Z.
+Notation "x == y"  := (Zeq x y) (at level 70) : IntScope.
+Notation "x ~= y" := (~ Zeq x y) (at level 70) : IntScope.
+Notation "0" := Z0 : IntScope.
+Notation "1" := (Zsucc Z0) : IntScope.
+Notation "x + y" := (Zplus x y) : IntScope.
+Notation "x - y" := (Zminus x y) : IntScope.
+Notation "x * y" := (Ztimes x y) : IntScope.
+Notation "x < y" := (Zlt x y) : IntScope.
+Notation "x <= y" := (Zle x y) : IntScope.
+Notation "x > y" := (Zlt y x) (only parsing) : IntScope.
+Notation "x >= y" := (Zle y x) (only parsing) : IntScope.
+
+Notation Local N := NZ.
+(* To remember N without having to use a long qualifying name. since NZ will be redefined *)
+Notation Local NE := NZE (only parsing).
+Notation Local plus_wd := NZplus_wd (only parsing).
+
+Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
+Module Export NZAxiomsMod <: NZAxiomsSig.
+
+Definition NZ : Set := Z.
+Definition NZE := Zeq.
+Definition NZ0 := Z0.
+Definition NZsucc := Zsucc.
+Definition NZpred := Zpred.
+Definition NZplus := Zplus.
+Definition NZminus := Zminus.
+Definition NZtimes := Ztimes.
+
+Theorem ZE_refl : reflexive Z Zeq.
 Proof.
-unfold reflexive, E; reflexivity.
+unfold reflexive, Zeq. reflexivity.
 Qed.
 
-Theorem ZE_symm : symmetric Z E.
+Theorem ZE_symm : symmetric Z Zeq.
 Proof.
-unfold symmetric, E; now symmetry.
+unfold symmetric, Zeq; now symmetry.
 Qed.
 
-Theorem ZE_trans : transitive Z E.
+Theorem ZE_trans : transitive Z Zeq.
 Proof.
-unfold transitive, E. intros n m p H1 H2.
+unfold transitive, Zeq. intros n m p H1 H2.
 assert (H3 : (fst n + snd m) + (fst m + snd p) == (fst m + snd n) + (fst p + snd m))
 by now apply plus_wd.
 stepl ((fst n + snd p) + (fst m + snd m)) in H3 by ring.
@@ -50,46 +84,46 @@ stepr ((fst p + snd n) + (fst m + snd m)) in H3 by ring.
 now apply -> plus_cancel_r in H3.
 Qed.
 
-Theorem NZE_equiv : equiv Z E.
+Theorem NZE_equiv : equiv Z Zeq.
 Proof.
 unfold equiv; repeat split; [apply ZE_refl | apply ZE_trans | apply ZE_symm].
 Qed.
 
-Add Relation Z E
+Add Relation Z Zeq
  reflexivity proved by (proj1 NZE_equiv)
  symmetry proved by (proj2 (proj2 NZE_equiv))
  transitivity proved by (proj1 (proj2 NZE_equiv))
 as NZE_rel.
 
-Add Morphism (@pair N N) with signature NE ==> NE ==> E as Zpair_wd.
+Add Morphism (@pair N N) with signature NE ==> NE ==> Zeq as Zpair_wd.
 Proof.
-intros n1 n2 H1 m1 m2 H2; unfold E; simpl; rewrite H1; now rewrite H2.
+intros n1 n2 H1 m1 m2 H2; unfold Zeq; simpl; rewrite H1; now rewrite H2.
 Qed.
 
-Add Morphism NZsucc with signature E ==> E as NZsucc_wd.
+Add Morphism NZsucc with signature Zeq ==> Zeq as NZsucc_wd.
 Proof.
-unfold NZsucc, E; intros n m H; simpl.
+unfold NZsucc, Zeq; intros n m H; simpl.
 do 2 rewrite plus_succ_l; now rewrite H.
 Qed.
 
-Add Morphism NZpred with signature E ==> E as NZpred_wd.
+Add Morphism NZpred with signature Zeq ==> Zeq as NZpred_wd.
 Proof.
-unfold NZpred, E; intros n m H; simpl.
+unfold NZpred, Zeq; intros n m H; simpl.
 do 2 rewrite plus_succ_r; now rewrite H.
 Qed.
 
-Add Morphism NZplus with signature E ==> E ==> E as NZplus_wd.
+Add Morphism NZplus with signature Zeq ==> Zeq ==> Zeq as NZplus_wd.
 Proof.
-unfold E, NZplus; intros n1 m1 H1 n2 m2 H2; simpl.
+unfold Zeq, NZplus; intros n1 m1 H1 n2 m2 H2; simpl.
 assert (H3 : (fst n1 + snd m1) + (fst n2 + snd m2) == (fst m1 + snd n1) + (fst m2 + snd n2))
 by now apply plus_wd.
 stepl (fst n1 + snd m1 + (fst n2 + snd m2)) by ring.
 now stepr (fst m1 + snd n1 + (fst m2 + snd n2)) by ring.
 Qed.
 
-Add Morphism NZminus with signature E ==> E ==> E as NZminus_wd.
+Add Morphism NZminus with signature Zeq ==> Zeq ==> Zeq as NZminus_wd.
 Proof.
-unfold E, NZminus; intros n1 m1 H1 n2 m2 H2; simpl.
+unfold Zeq, NZminus; intros n1 m1 H1 n2 m2 H2; simpl.
 symmetry in H2.
 assert (H3 : (fst n1 + snd m1) + (fst m2 + snd n2) == (fst m1 + snd n1) + (fst n2 + snd m2))
 by now apply plus_wd.
@@ -97,9 +131,9 @@ stepl (fst n1 + snd m1 + (fst m2 + snd n2)) by ring.
 now stepr (fst m1 + snd n1 + (fst n2 + snd m2)) by ring.
 Qed.
 
-Add Morphism NZtimes with signature E ==> E ==> E as NZtimes_wd.
+Add Morphism NZtimes with signature Zeq ==> Zeq ==> Zeq as NZtimes_wd.
 Proof.
-unfold NZtimes, E; intros n1 m1 H1 n2 m2 H2; simpl.
+unfold NZtimes, Zeq; intros n1 m1 H1 n2 m2 H2; simpl.
 stepl (fst n1 * fst n2 + (snd n1 * snd n2 + fst m1 * snd m2 + snd m1 * fst m2)) by ring.
 stepr (fst n1 * snd n2 + (fst m1 * fst m2 + snd m1 * snd m2 + snd n1 * fst n2)) by ring.
 apply plus_times_repl_pair with (n := fst m2) (m := snd m2); [| now idtac].
@@ -117,39 +151,20 @@ apply plus_times_repl_pair with (n := fst m1) (m := snd m1); [| now idtac].
 ring.
 Qed.
 
-Delimit Scope IntScope with Int.
-Bind Scope IntScope with NZ.
-Open Local Scope IntScope.
-Notation "x == y"  := (NZE x y) (at level 70) : IntScope.
-Notation "x ~= y" := (~ NZE x y) (at level 70) : IntScope.
-Notation "0" := NZ0 : IntScope.
-Notation "'S'" := NZsucc : IntScope.
-Notation "'P'" := NZpred : IntScope.
-Notation "1" := (S 0) : IntScope.
-Notation "x + y" := (NZplus x y) : IntScope.
-Notation "x - y" := (NZminus x y) : IntScope.
-Notation "x * y" := (NZtimes x y) : IntScope.
-
-Theorem NZpred_succ : forall n : Z, P (S n) == n.
-Proof.
-unfold NZpred, NZsucc, E; intro n; simpl.
-rewrite plus_succ_l; now rewrite plus_succ_r.
-Qed.
-
 Section Induction.
 Open Scope NatIntScope. (* automatically closes at the end of the section *)
 Variable A : Z -> Prop.
-Hypothesis A_wd : predicate_wd E A.
+Hypothesis A_wd : predicate_wd Zeq A.
 
-Add Morphism A with signature E ==> iff as A_morph.
+Add Morphism A with signature Zeq ==> iff as A_morph.
 Proof.
 exact A_wd.
 Qed.
 
 Theorem NZinduction :
-  A 0 -> (forall n : Z, A n <-> A (S n)) -> forall n : Z, A n. (* 0 is interpreted as in Z due to "Bind" directive *)
+  A 0 -> (forall n : Z, A n <-> A (Zsucc n)) -> forall n : Z, A n. (* 0 is interpreted as in Z due to "Bind" directive *)
 Proof.
-intros A0 AS n; unfold NZ0, NZsucc, predicate_wd, fun_wd, E in *.
+intros A0 AS n; unfold NZ0, Zsucc, predicate_wd, fun_wd, Zeq in *.
 destruct n as [n m].
 cut (forall p : N, A (p, 0)); [intro H1 |].
 cut (forall p : N, A (0, p)); [intro H2 |].
@@ -166,51 +181,56 @@ Qed.
 
 End Induction.
 
+(* Time to prove theorems in the language of Z *)
+
+Open Local Scope IntScope.
+
+Theorem NZpred_succ : forall n : Z, Zpred (Zsucc n) == n.
+Proof.
+unfold NZpred, NZsucc, Zeq; intro n; simpl.
+rewrite plus_succ_l; now rewrite plus_succ_r.
+Qed.
+
 Theorem NZplus_0_l : forall n : Z, 0 + n == n.
 Proof.
-intro n; unfold NZplus, E; simpl. now do 2 rewrite plus_0_l.
+intro n; unfold NZplus, Zeq; simpl. now do 2 rewrite plus_0_l.
 Qed.
 
-Theorem NZplus_succ_l : forall n m : Z, (S n) + m == S (n + m).
+Theorem NZplus_succ_l : forall n m : Z, (Zsucc n) + m == Zsucc (n + m).
 Proof.
-intros n m; unfold NZplus, E; simpl. now do 2 rewrite plus_succ_l.
+intros n m; unfold NZplus, Zeq; simpl. now do 2 rewrite plus_succ_l.
 Qed.
 
 Theorem NZminus_0_r : forall n : Z, n - 0 == n.
 Proof.
-intro n; unfold NZminus, E; simpl. now do 2 rewrite plus_0_r.
+intro n; unfold NZminus, Zeq; simpl. now do 2 rewrite plus_0_r.
 Qed.
 
-Theorem NZminus_succ_r : forall n m : Z, n - (S m) == P (n - m).
+Theorem NZminus_succ_r : forall n m : Z, n - (Zsucc m) == Zpred (n - m).
 Proof.
-intros n m; unfold NZminus, E; simpl. symmetry; now rewrite plus_succ_r.
+intros n m; unfold NZminus, Zeq; simpl. symmetry; now rewrite plus_succ_r.
 Qed.
 
 Theorem NZtimes_0_r : forall n : Z, n * 0 == 0.
 Proof.
-intro n; unfold NZtimes, E; simpl.
+intro n; unfold NZtimes, Zeq; simpl.
 repeat rewrite times_0_r. now rewrite plus_assoc.
 Qed.
 
-Theorem NZtimes_succ_r : forall n m : Z, n * (S m) == n * m + n.
+Theorem NZtimes_succ_r : forall n m : Z, n * (Zsucc m) == n * m + n.
 Proof.
-intros n m; unfold NZtimes, NZsucc, E; simpl.
+intros n m; unfold NZtimes, NZsucc, Zeq; simpl.
 do 2 rewrite times_succ_r. ring.
 Qed.
 
 End NZAxiomsMod.
 
-Definition NZlt (n m : Z) := (fst n) + (snd m) < (fst m) + (snd n).
-Definition NZle (n m : Z) := (fst n) + (snd m) <= (fst m) + (snd n).
-
-Notation "x < y" := (NZlt x y) : IntScope.
-Notation "x <= y" := (NZle x y) : IntScope.
-Notation "x > y" := (NZlt y x) (only parsing) : IntScope.
-Notation "x >= y" := (NZle y x) (only parsing) : IntScope.
+Definition NZlt := Zlt.
+Definition NZle := Zle.
 
-Add Morphism NZlt with signature E ==> E ==> iff as NZlt_wd.
+Add Morphism NZlt with signature Zeq ==> Zeq ==> iff as NZlt_wd.
 Proof.
-unfold NZlt, E; intros n1 m1 H1 n2 m2 H2; simpl. split; intro H.
+unfold NZlt, Zlt, Zeq; intros n1 m1 H1 n2 m2 H2; simpl. split; intro H.
 stepr (snd m1 + fst m2) by apply plus_comm.
 apply (plus_lt_repl_pair (fst n1) (snd n1)); [| assumption].
 stepl (snd m2 + fst n1) by apply plus_comm.
@@ -227,58 +247,58 @@ now stepl (fst m1 + snd m2) by apply plus_comm.
 stepl (fst n2 + snd m2) by apply plus_comm. now stepr (fst m2 + snd n2) by apply plus_comm.
 Qed.
 
-Open Local Scope IntScope.
-
-Add Morphism NZle with signature E ==> E ==> iff as NZle_wd.
+Add Morphism NZle with signature Zeq ==> Zeq ==> iff as NZle_wd.
 Proof.
-unfold NZle, E; intros n1 m1 H1 n2 m2 H2; simpl.
-do 2 rewrite le_lt_or_eq. rewrite (NZlt_wd n1 m1 H1 n2 m2 H2). fold (m1 < m2).
-fold (n1 == n2) (m1 == m2); fold (n1 == m1) in H1; fold (n2 == m2) in H2.
+unfold NZle, Zle, Zeq; intros n1 m1 H1 n2 m2 H2; simpl.
+do 2 rewrite le_lt_or_eq. rewrite (NZlt_wd n1 m1 H1 n2 m2 H2). fold (m1 < m2)%Int.
+fold (n1 == n2)%Int (m1 == m2)%Int; fold (n1 == m1)%Int in H1; fold (n2 == m2)%Int in H2.
 now rewrite H1, H2.
 Qed.
 
+Open Local Scope IntScope.
+
 Theorem NZle_lt_or_eq : forall n m : Z, n <= m <-> n < m \/ n == m.
 Proof.
-intros n m; unfold NZlt, NZle, E; simpl. apply le_lt_or_eq.
+intros n m; unfold Zlt, Zle, Zeq; simpl. apply le_lt_or_eq.
 Qed.
 
 Theorem NZlt_irrefl : forall n : Z, ~ (n < n).
 Proof.
-intros n; unfold NZlt, E; simpl. apply lt_irrefl.
+intros n; unfold Zlt, Zeq; simpl. apply lt_irrefl.
 Qed.
 
-Theorem NZlt_succ_le : forall n m : Z, n < (S m) <-> n <= m.
+Theorem NZlt_succ_le : forall n m : Z, n < (Zsucc m) <-> n <= m.
 Proof.
-intros n m; unfold NZlt, NZle, E; simpl. rewrite plus_succ_l; apply lt_succ_le.
+intros n m; unfold Zlt, Zle, Zeq; simpl. rewrite plus_succ_l; apply lt_succ_le.
 Qed.
 
 End NZOrdAxiomsMod.
 
-Definition Zopp (n : Z) := (snd n, fst n).
+Definition Zopp (n : Z) : Z := (snd n, fst n).
 
-Notation "- x" := (Zopp x) (at level 35, right associativity) : IntScope.
+Notation "- x" := (Zopp x) : IntScope.
 
-Add Morphism Zopp with signature E ==> E as Zopp_wd.
+Add Morphism Zopp with signature Zeq ==> Zeq as Zopp_wd.
 Proof.
-unfold E; intros n m H; simpl. symmetry.
+unfold Zeq; intros n m H; simpl. symmetry.
 stepl (fst n + snd m) by apply plus_comm.
 now stepr (fst m + snd n) by apply plus_comm.
 Qed.
 
 Open Local Scope IntScope.
 
-Theorem Zsucc_pred : forall n : Z, S (P n) == n.
+Theorem Zsucc_pred : forall n : Z, Zsucc (Zpred n) == n.
 Proof.
-intro n; unfold NZsucc, NZpred, E; simpl.
+intro n; unfold Zsucc, Zpred, Zeq; simpl.
 rewrite plus_succ_l; now rewrite plus_succ_r.
 Qed.
 
 Theorem Zopp_0 : - 0 == 0.
 Proof.
-unfold Zopp, E; simpl. now rewrite plus_0_l.
+unfold Zopp, Zeq; simpl. now rewrite plus_0_l.
 Qed.
 
-Theorem Zopp_succ : forall n, - (S n) == P (- n).
+Theorem Zopp_succ : forall n, - (Zsucc n) == Zpred (- n).
 Proof.
 reflexivity.
 Qed.
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 5c6369fe4..cb3dd3093 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -44,6 +44,13 @@ Proof.
 intros n m H1 H2; rewrite H2 in H1; false_hyp H1 NZlt_irrefl.
 Qed.
 
+Theorem NZlt_le_neq : forall n m : NZ, n < m <-> n <= m /\ n ~= m.
+Proof.
+intros n m; split; [intro H | intros [H1 H2]].
+split. le_less. now apply NZlt_neq.
+le_elim H1. assumption. false_hyp H1 H2.
+Qed.
+
 Theorem NZle_refl : forall n : NZ, n <= n.
 Proof.
 intro; now le_equal.
diff --git a/theories/Numbers/NatInt/NZPlusOrder.v b/theories/Numbers/NatInt/NZPlusOrder.v
deleted file mode 100644
index 6368fa557..000000000
--- a/theories/Numbers/NatInt/NZPlusOrder.v
+++ /dev/null
@@ -1,67 +0,0 @@
-Require Export NZPlus.
-Require Export NZOrder.
-
-Module NZPlusOrderPropFunct
-  (Import NZPlusMod : NZPlusSig)
-  (Import NZOrderMod : NZOrderSig with Module NZBaseMod := NZPlusMod.NZBaseMod).
-
-Module Export NZPlusPropMod := NZPlusPropFunct NZPlusMod.
-Module Export NZOrderPropMod := NZOrderPropFunct NZOrderMod.
-Open Local Scope NatIntScope.
-
-Theorem NZplus_lt_mono_l : forall n m p, n < m <-> p + n < p + m.
-Proof.
-intros n m p; NZinduct p.
-now do 2 rewrite NZplus_0_l.
-intro p. do 2 rewrite NZplus_succ_l. now rewrite <- NZsucc_lt_mono.
-Qed.
-
-Theorem NZplus_lt_mono_r : forall n m p, n < m <-> n + p < m + p.
-Proof.
-intros n m p.
-rewrite (NZplus_comm n p); rewrite (NZplus_comm m p); apply NZplus_lt_mono_l.
-Qed.
-
-Theorem NZplus_lt_mono : forall n m p q, n < m -> p < q -> n + p < m + q.
-Proof.
-intros n m p q H1 H2.
-apply NZlt_trans with (m + p);
-[now apply -> NZplus_lt_mono_r | now apply -> NZplus_lt_mono_l].
-Qed.
-
-Theorem NZplus_le_mono_l : forall n m p, n <= m <-> p + n <= p + m.
-Proof.
-intros n m p; NZinduct p.
-now do 2 rewrite NZplus_0_l.
-intro p. do 2 rewrite NZplus_succ_l. now rewrite <- NZsucc_le_mono.
-Qed.
-
-Theorem NZplus_le_mono_r : forall n m p, n <= m <-> n + p <= m + p.
-Proof.
-intros n m p.
-rewrite (NZplus_comm n p); rewrite (NZplus_comm m p); apply NZplus_le_mono_l.
-Qed.
-
-Theorem NZplus_le_mono : forall n m p q, n <= m -> p <= q -> n + p <= m + q.
-Proof.
-intros n m p q H1 H2.
-apply NZle_trans with (m + p);
-[now apply -> NZplus_le_mono_r | now apply -> NZplus_le_mono_l].
-Qed.
-
-Theorem NZplus_lt_le_mono : forall n m p q, n < m -> p <= q -> n + p < m + q.
-Proof.
-intros n m p q H1 H2.
-apply NZlt_le_trans with (m + p);
-[now apply -> NZplus_lt_mono_r | now apply -> NZplus_le_mono_l].
-Qed.
-
-Theorem NZplus_le_lt_mono : forall n m p q, n <= m -> p < q -> n + p < m + q.
-Proof.
-intros n m p q H1 H2.
-apply NZle_lt_trans with (m + p);
-[now apply -> NZplus_le_mono_r | now apply -> NZplus_lt_mono_l].
-Qed.
-
-End NZPlusOrderPropFunct.
-
diff --git a/theories/Numbers/NatInt/NZTimesOrder.v b/theories/Numbers/NatInt/NZTimesOrder.v
index 6f702067d..2f3cf678b 100644
--- a/theories/Numbers/NatInt/NZTimesOrder.v
+++ b/theories/Numbers/NatInt/NZTimesOrder.v
@@ -61,6 +61,37 @@ apply NZle_lt_trans with (m + p);
 [now apply -> NZplus_le_mono_r | now apply -> NZplus_lt_mono_l].
 Qed.
 
+Theorem NZplus_pos_pos : forall n m : NZ, 0 < n -> 0 < m -> 0 < n + m.
+Proof.
+intros n m H1 H2. rewrite <- (NZplus_0_l 0). now apply NZplus_lt_mono.
+Qed.
+
+Theorem NZplus_pos_nonneg : forall n m : NZ, 0 < n -> 0 <= m -> 0 < n + m.
+Proof.
+intros n m H1 H2. rewrite <- (NZplus_0_l 0). now apply NZplus_lt_le_mono.
+Qed.
+
+Theorem NZplus_nonneg_pos : forall n m : NZ, 0 <= n -> 0 < m -> 0 < n + m.
+Proof.
+intros n m H1 H2. rewrite <- (NZplus_0_l 0). now apply NZplus_le_lt_mono.
+Qed.
+
+Theorem NZplus_nonneg_nonneg : forall n m : NZ, 0 <= n -> 0 <= m -> 0 <= n + m.
+Proof.
+intros n m H1 H2. rewrite <- (NZplus_0_l 0). now apply NZplus_le_mono.
+Qed.
+
+Theorem NZlt_plus_pos_l : forall n m : NZ, 0 < n -> m < n + m.
+Proof.
+intros n m H. apply -> (NZplus_lt_mono_r 0 n m) in H.
+now rewrite NZplus_0_l in H.
+Qed.
+
+Theorem NZlt_plus_pos_r : forall n m : NZ, 0 < n -> m < m + n.
+Proof.
+intros; rewrite NZplus_comm; now apply NZlt_plus_pos_l.
+Qed.
+
 Theorem NZle_lt_plus_lt : forall n m p q : NZ, n <= m -> p + m < q + n -> p < q.
 Proof.
 intros n m p q H1 H2. destruct (NZle_gt_cases q p); [| assumption].
@@ -75,7 +106,7 @@ pose proof (NZplus_le_lt_mono q p n m H H1) as H3. apply <- NZnle_gt in H3.
 false_hyp H2 H3.
 Qed.
 
-Theorem NZle_le_plus_lt : forall n m p q : NZ, n <= m -> p + m <= q + n -> p <= q.
+Theorem NZle_le_plus_le : forall n m p q : NZ, n <= m -> p + m <= q + n -> p <= q.
 Proof.
 intros n m p q H1 H2. destruct (NZle_gt_cases p q); [assumption |].
 pose proof (NZplus_lt_le_mono q p n m H H1) as H3. apply <- NZnle_gt in H3.
@@ -370,4 +401,14 @@ elimtype False; now apply (NZlt_asymm (n * m) 0).
 now apply NZtimes_neg_pos. now apply NZtimes_pos_neg.
 Qed.
 
+Theorem NZtimes_2_mono_l : forall n m : NZ, n < m -> 1 + (1 + 1) * n < (1 + 1) * m.
+Proof.
+intros n m H. apply -> NZlt_le_succ in H.
+apply -> (NZtimes_le_mono_pos_l (S n) m (1 + 1)) in H.
+repeat rewrite NZtimes_plus_distr_r in *; repeat rewrite NZtimes_1_l in *.
+repeat rewrite NZplus_succ_r in *. repeat rewrite NZplus_succ_l in *. rewrite NZplus_0_l.
+now apply <- NZlt_le_succ.
+apply NZplus_pos_pos; now apply NZlt_succ_r.
+Qed.
+
 End NZTimesOrderPropFunct.
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index f62b5ecb2..7c2610ccc 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -25,6 +25,9 @@ Proof NZlt_le_incl.
 Theorem lt_neq : forall n m : N, n < m -> n ~= m.
 Proof NZlt_neq.
 
+Theorem lt_le_neq : forall n m : N, n < m <-> n <= m /\ n ~= m.
+Proof NZlt_le_neq.
+
 Theorem le_refl : forall n : N, n <= n.
 Proof NZle_refl.
 
diff --git a/theories/Numbers/Natural/Abstract/NPlusOrder.v b/theories/Numbers/Natural/Abstract/NPlusOrder.v
deleted file mode 100644
index c4640858e..000000000
--- a/theories/Numbers/Natural/Abstract/NPlusOrder.v
+++ /dev/null
@@ -1,87 +0,0 @@
-Require Export NPlus.
-Require Export NOrder.
-Require Import NZPlusOrder.
-
-Module NPlusOrderPropFunct
-  (Import NPlusMod : NPlusSig)
-  (Import NOrderMod : NOrderSig with Module NAxiomsMod := NPlusMod.NAxiomsMod).
-Module Export NPlusPropMod := NPlusPropFunct NPlusMod.
-Module Export NOrderPropMod := NOrderPropFunct NOrderMod.
-Module Export NZPlusOrderPropMod := NZPlusOrderPropFunct NZPlusMod NZOrderMod.
-Open Local Scope NatScope.
-
-(* Print All locks up here !!! *)
-Theorem lt_plus_trans : forall n m p, n < m -> n < m + p.
-Proof.
-intros n m p; induct p.
-now rewrite plus_0_r.
-intros x IH H.
-rewrite plus_succ_r. apply lt_closed_succ. apply IH; apply H.
-Qed.
-
-Theorem plus_lt_compat_l : forall n m p, n < m -> p + n < p + m.
-Proof.
-intros n m p H; induct p.
-do 2 rewrite plus_0_l; assumption.
-intros x IH. do 2 rewrite plus_succ_l. now apply <- lt_resp_succ.
-Qed.
-
-Theorem plus_lt_compat_r : forall n m p, n < m -> n + p < m + p.
-Proof.
-intros n m p H; rewrite plus_comm.
-set (k := p + n); rewrite plus_comm; unfold k; clear k.
-now apply plus_lt_compat_l.
-Qed.
-
-Theorem plus_lt_compat : forall n m p q, n < m -> p < q -> n + p < m + q.
-Proof.
-intros n m p q H1 H2.
-apply lt_trans with (m := m + p);
-[now apply plus_lt_compat_r | now apply plus_lt_compat_l].
-Qed.
-
-Theorem plus_lt_cancel_l : forall p n m, p + n < p + m <-> n < m.
-Proof.
-intros p n m; induct p.
-now do 2 rewrite plus_0_l.
-intros p IH.
-do 2 rewrite plus_succ_l. now rewrite lt_resp_succ.
-Qed.
-
-Theorem plus_lt_cancel_r : forall p n m, n + p < m + p <-> n < m.
-Proof.
-intros p n m;
-setoid_replace (n + p) with (p + n) by apply plus_comm;
-setoid_replace (m + p) with (p + m) by apply plus_comm;
-apply plus_lt_cancel_l.
-Qed.
-
-(* The following property is similar to plus_repl_pair in NPlus.v
-and is used to prove the correctness of the definition of order
-on integers constructed from pairs of natural numbers *)
-
-Theorem plus_lt_repl_pair : forall n m n' m' u v,
-  n + u < m + v -> n + m' == n' + m -> n' + u < m' + v.
-Proof.
-intros n m n' m' u v H1 H2.
-apply <- (plus_lt_cancel_r (n + m')) in H1.
-set (k := n + m') in H1 at 2; rewrite H2 in H1; unfold k in H1; clear k.
-rewrite <- plus_assoc in H1.
-setoid_replace (m + v + (n + m')) with (n + m' + (m + v)) in H1 by apply plus_comm.
-rewrite <- plus_assoc in H1. apply -> plus_lt_cancel_l in H1.
-rewrite plus_assoc in H1. setoid_replace (m + v) with (v + m) in H1 by apply plus_comm.
-rewrite plus_assoc in H1. apply -> plus_lt_cancel_r in H1.
-now rewrite plus_comm in H1.
-Qed.
-
-Theorem plus_gt_succ :
-  forall n m p, S p < n + m -> (exists n', n == S n') \/ (exists m', m == S m').
-Proof.
-intros n m p H.
-apply <- lt_le_succ in H.
-apply lt_exists_pred in H. destruct H as [q H].
-now apply plus_eq_succ in H.
-Qed.
-
-End NPlusOrderProperties.
-
diff --git a/theories/Numbers/Natural/Abstract/NTimesOrder.v b/theories/Numbers/Natural/Abstract/NTimesOrder.v
index 2dbfd8f97..dc1b977aa 100644
--- a/theories/Numbers/Natural/Abstract/NTimesOrder.v
+++ b/theories/Numbers/Natural/Abstract/NTimesOrder.v
@@ -28,22 +28,31 @@ Proof NZplus_lt_le_mono.
 Theorem plus_le_lt_mono : forall n m p q : N, n <= m -> p < q -> n + p < m + q.
 Proof NZplus_le_lt_mono.
 
+Theorem plus_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n + m.
+Proof NZplus_pos_pos.
+
+Theorem lt_plus_pos_l : forall n m : N, 0 < n -> m < n + m.
+Proof NZlt_plus_pos_l.
+
+Theorem lt_plus_pos_r : forall n m : N, 0 < n -> m < m + n.
+Proof NZlt_plus_pos_r.
+
 Theorem le_lt_plus_lt : forall n m p q : N, n <= m -> p + m < q + n -> p < q.
 Proof NZle_lt_plus_lt.
 
 Theorem lt_le_plus_lt : forall n m p q : N, n < m -> p + m <= q + n -> p < q.
 Proof NZlt_le_plus_lt.
 
-Theorem le_le_plus_lt : forall n m p q : N, n <= m -> p + m <= q + n -> p <= q.
-Proof NZle_le_plus_lt.
+Theorem le_le_plus_le : forall n m p q : N, n <= m -> p + m <= q + n -> p <= q.
+Proof NZle_le_plus_le.
 
 Theorem plus_lt_cases : forall n m p q : N, n + m < p + q -> n < p \/ m < q.
 Proof NZplus_lt_cases.
 
-Theorem plus_le_cases : forall n m p q : NZ, n + m <= p + q -> n <= p \/ m <= q.
+Theorem plus_le_cases : forall n m p q : N, n + m <= p + q -> n <= p \/ m <= q.
 Proof NZplus_le_cases.
 
-Theorem plus_pos_cases : forall n m : NZ, 0 < n + m -> 0 < n \/ 0 < m.
+Theorem plus_pos_cases : forall n m : N, 0 < n + m -> 0 < n \/ 0 < m.
 Proof NZplus_pos_cases.
 
 (** Theorems true for natural numbers *)
@@ -55,17 +64,25 @@ rewrite plus_0_r; le_equal.
 intros m IH. rewrite plus_succ_r; now apply le_le_succ.
 Qed.
 
-Theorem lt_plus_r : forall n m : N, m ~= 0 -> n < n + m.
+Theorem lt_lt_plus_r : forall n m p : N, n < m -> n < m + p.
 Proof.
-intros n m; cases m.
-intro H; elimtype False; now apply H.
-intros. rewrite plus_succ_r. apply <- lt_succ_le. apply le_plus_r.
+intros n m p H; rewrite <- (plus_0_r n).
+apply plus_lt_le_mono; [assumption | apply le_0_l].
 Qed.
 
-Theorem lt_lt_plus : forall n m p : N, n < m -> n < m + p.
+Theorem lt_lt_plus_l : forall n m p : N, n < m -> n < p + m.
 Proof.
-intros n m p H; rewrite <- (plus_0_r n).
-apply plus_lt_le_mono; [assumption | apply le_0_l].
+intros n m p; rewrite plus_comm; apply lt_lt_plus_r.
+Qed.
+
+Theorem plus_pos_l : forall n m : N, 0 < n -> 0 < n + m.
+Proof.
+intros; apply NZplus_pos_nonneg. assumption. apply le_0_l.
+Qed.
+
+Theorem plus_pos_r : forall n m : N, 0 < m -> 0 < n + m.
+Proof.
+intros; apply NZplus_nonneg_pos. apply le_0_l. assumption.
 Qed.
 
 (* The following property is similar to plus_repl_pair in NPlus.v
@@ -123,7 +140,7 @@ Proof.
 intros; apply NZtimes_le_mono; try assumption; apply le_0_l.
 Qed.
 
-Theorem times_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n * m.
+Theorem Ztimes_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n * m.
 Proof NZtimes_pos_pos.
 
 Theorem times_eq_0 : forall n m : N, n * m == 0 -> n == 0 \/ m == 0.
@@ -132,11 +149,14 @@ Proof NZtimes_eq_0.
 Theorem times_neq_0 : forall n m : N, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
 Proof NZtimes_neq_0.
 
+Theorem times_2_mono_l : forall n m : N, n < m -> 1 + (1 + 1) * n < (1 + 1) * m.
+Proof NZtimes_2_mono_l.
+
 Theorem times_pos : forall n m : N, n * m > 0 <-> n > 0 /\ m > 0.
 Proof.
 intros n m; split; [intro H | intros [H1 H2]].
 apply -> NZtimes_pos in H. destruct H as [[H1 H2] | [H1 H2]]. now split. false_hyp H1 nlt_0_r.
-now apply times_pos_pos.
+now apply NZtimes_pos_pos.
 Qed.
 
 End NTimesOrderPropFunct.