Simplification of Numbers, mainly thanks to Include

 - No more nesting of Module and Module Type, we rather use Include.
 - Instead of in-name-qualification like NZeq, we use uniform
   short names + modular qualification like N.eq when necessary.
 - Many simplification of proofs, by some autorewrite for instance
 - In NZOrder, we instantiate an "order" tactic.
 - Some requirements in NZAxioms were superfluous: compatibility
   of le, min and max could be derived from the rest.
 - NMul removed, since it was containing only an ad-hoc result for
   ZNatPairs, that we've inlined in the proof of mul_wd there.
 - Zdomain removed (was already not compiled), idea of a module
   with eq and eqb reused in DecidableType.BooleanEqualityType.
 - ZBinDefs don't contain any definition now, migrate it to ZBinary.

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

8 files changed, 760 insertions, 747 deletions

diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v
index 9c852bf908..f7e6699aba 100644
--- a/theories/Numbers/NatInt/NZAdd.v
+++ b/theories/Numbers/NatInt/NZAdd.v
@@ -13,78 +13,78 @@
 Require Import NZAxioms.
 Require Import NZBase.
 
-Module NZAddPropFunct (Import NZAxiomsMod : NZAxiomsSig).
-Module Export NZBasePropMod := NZBasePropFunct NZAxiomsMod.
-Open Local Scope NatIntScope.
+Module NZAddPropFunct (Import NZ : NZAxiomsSig).
+Include NZBasePropFunct NZ.
+Local Open Scope NumScope.
 
-Theorem NZadd_0_r : forall n : NZ, n + 0 == n.
+Hint Rewrite
+ pred_succ add_0_l add_succ_l mul_0_l mul_succ_l sub_0_r sub_succ_r : nz.
+Ltac nzsimpl := autorewrite with nz.
+
+Theorem add_0_r : forall n, n + 0 == n.
 Proof.
-NZinduct n. now rewrite NZadd_0_l.
-intro. rewrite NZadd_succ_l. now rewrite NZsucc_inj_wd.
+nzinduct n. now nzsimpl.
+intro. nzsimpl. now rewrite succ_inj_wd.
 Qed.
 
-Theorem NZadd_succ_r : forall n m : NZ, n + S m == S (n + m).
+Theorem add_succ_r : forall n m, n + S m == S (n + m).
 Proof.
-intros n m; NZinduct n.
-now do 2 rewrite NZadd_0_l.
-intro. repeat rewrite NZadd_succ_l. now rewrite NZsucc_inj_wd.
+intros n m; nzinduct n. now nzsimpl.
+intro. nzsimpl. now rewrite succ_inj_wd.
 Qed.
 
-Theorem NZadd_comm : forall n m : NZ, n + m == m + n.
+Hint Rewrite add_0_r add_succ_r : nz.
+
+Theorem add_comm : forall n m, n + m == m + n.
 Proof.
-intros n m; NZinduct n.
-rewrite NZadd_0_l; now rewrite NZadd_0_r.
-intros n. rewrite NZadd_succ_l; rewrite NZadd_succ_r. now rewrite NZsucc_inj_wd.
+intros n m; nzinduct n. now nzsimpl.
+intro. nzsimpl. now rewrite succ_inj_wd.
 Qed.
 
-Theorem NZadd_1_l : forall n : NZ, 1 + n == S n.
+Theorem add_1_l : forall n, 1 + n == S n.
 Proof.
-intro n; rewrite NZadd_succ_l; now rewrite NZadd_0_l.
+intro n; now nzsimpl.
 Qed.
 
-Theorem NZadd_1_r : forall n : NZ, n + 1 == S n.
+Theorem add_1_r : forall n, n + 1 == S n.
 Proof.
-intro n; rewrite NZadd_comm; apply NZadd_1_l.
+intro n; now nzsimpl.
 Qed.
 
-Theorem NZadd_assoc : forall n m p : NZ, n + (m + p) == (n + m) + p.
+Theorem add_assoc : forall n m p, n + (m + p) == (n + m) + p.
 Proof.
-intros n m p; NZinduct n.
-now do 2 rewrite NZadd_0_l.
-intro. do 3 rewrite NZadd_succ_l. now rewrite NZsucc_inj_wd.
+intros n m p; nzinduct n. now nzsimpl.
+intro. nzsimpl. now rewrite succ_inj_wd.
 Qed.
 
-Theorem NZadd_shuffle1 : forall n m p q : NZ, (n + m) + (p + q) == (n + p) + (m + q).
+Theorem add_cancel_l : forall n m p, p + n == p + m <-> n == m.
 Proof.
-intros n m p q.
-rewrite <- (NZadd_assoc n m (p + q)). rewrite (NZadd_comm m (p + q)).
-rewrite <- (NZadd_assoc p q m). rewrite (NZadd_assoc n p (q + m)).
-now rewrite (NZadd_comm q m).
+intros n m p; nzinduct p. now nzsimpl.
+intro p. nzsimpl. now rewrite succ_inj_wd.
 Qed.
 
-Theorem NZadd_shuffle2 : forall n m p q : NZ, (n + m) + (p + q) == (n + q) + (m + p).
+Theorem add_cancel_r : forall n m p, n + p == m + p <-> n == m.
 Proof.
-intros n m p q.
-rewrite <- (NZadd_assoc n m (p + q)). rewrite (NZadd_assoc m p q).
-rewrite (NZadd_comm (m + p) q). now rewrite <- (NZadd_assoc n q (m + p)).
+intros n m p. rewrite (add_comm n p), (add_comm m p). apply add_cancel_l.
 Qed.
 
-Theorem NZadd_cancel_l : forall n m p : NZ, p + n == p + m <-> n == m.
+Theorem add_shuffle1 : forall n m p q, (n + m) + (p + q) == (n + p) + (m + q).
 Proof.
-intros n m p; NZinduct p.
-now do 2 rewrite NZadd_0_l.
-intro p. do 2 rewrite NZadd_succ_l. now rewrite NZsucc_inj_wd.
+intros n m p q.
+rewrite <- (add_assoc n m), <- (add_assoc n p), add_cancel_l.
+rewrite 2 add_assoc, add_cancel_r. now apply add_comm.
 Qed.
 
-Theorem NZadd_cancel_r : forall n m p : NZ, n + p == m + p <-> n == m.
+Theorem add_shuffle2 : forall n m p q, (n + m) + (p + q) == (n + q) + (m + p).
 Proof.
-intros n m p. rewrite (NZadd_comm n p); rewrite (NZadd_comm m p).
-apply NZadd_cancel_l.
+intros n m p q.
+rewrite <- (add_assoc n m), <- (add_assoc n q), add_cancel_l.
+rewrite add_assoc. now apply add_comm.
 Qed.
 
-Theorem NZsub_1_r : forall n : NZ, n - 1 == P n.
+Theorem sub_1_r : forall n, n - 1 == P n.
 Proof.
-intro n; rewrite NZsub_succ_r; now rewrite NZsub_0_r.
+intro n; now nzsimpl.
 Qed.
 
 End NZAddPropFunct.
diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v
index d1caa83eeb..fcfbfd123c 100644
--- a/theories/Numbers/NatInt/NZAddOrder.v
+++ b/theories/Numbers/NatInt/NZAddOrder.v
@@ -10,156 +10,144 @@
 
 (*i $Id$ i*)
 
-Require Import NZAxioms.
-Require Import NZOrder.
+Require Import NZAxioms NZOrder.
 
-Module NZAddOrderPropFunct (Import NZOrdAxiomsMod : NZOrdAxiomsSig).
-Module Export NZOrderPropMod := NZOrderPropFunct NZOrdAxiomsMod.
-Open Local Scope NatIntScope.
+Module NZAddOrderPropFunct (Import NZ : NZOrdAxiomsSig).
+Include NZOrderPropFunct NZ.
+Local Open Scope NumScope.
 
-Theorem NZadd_lt_mono_l : forall n m p : NZ, n < m <-> p + n < p + m.
+Theorem add_lt_mono_l : forall n m p, n < m <-> p + n < p + m.
 Proof.
-intros n m p; NZinduct p.
-now do 2 rewrite NZadd_0_l.
-intro p. do 2 rewrite NZadd_succ_l. now rewrite <- NZsucc_lt_mono.
+intros n m p; nzinduct p. now nzsimpl.
+intro p. nzsimpl. now rewrite <- succ_lt_mono.
 Qed.
 
-Theorem NZadd_lt_mono_r : forall n m p : NZ, n < m <-> n + p < m + p.
+Theorem add_lt_mono_r : forall n m p, n < m <-> n + p < m + p.
 Proof.
-intros n m p.
-rewrite (NZadd_comm n p); rewrite (NZadd_comm m p); apply NZadd_lt_mono_l.
+intros n m p. rewrite (add_comm n p), (add_comm m p); apply add_lt_mono_l.
 Qed.
 
-Theorem NZadd_lt_mono : forall n m p q : NZ, n < m -> p < q -> n + p < m + q.
+Theorem add_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 -> NZadd_lt_mono_r | now apply -> NZadd_lt_mono_l].
+apply lt_trans with (m + p);
+[now apply -> add_lt_mono_r | now apply -> add_lt_mono_l].
 Qed.
 
-Theorem NZadd_le_mono_l : forall n m p : NZ, n <= m <-> p + n <= p + m.
+Theorem add_le_mono_l : forall n m p, n <= m <-> p + n <= p + m.
 Proof.
-intros n m p; NZinduct p.
-now do 2 rewrite NZadd_0_l.
-intro p. do 2 rewrite NZadd_succ_l. now rewrite <- NZsucc_le_mono.
+intros n m p; nzinduct p. now nzsimpl.
+intro p. nzsimpl. now rewrite <- succ_le_mono.
 Qed.
 
-Theorem NZadd_le_mono_r : forall n m p : NZ, n <= m <-> n + p <= m + p.
+Theorem add_le_mono_r : forall n m p, n <= m <-> n + p <= m + p.
 Proof.
-intros n m p.
-rewrite (NZadd_comm n p); rewrite (NZadd_comm m p); apply NZadd_le_mono_l.
+intros n m p. rewrite (add_comm n p), (add_comm m p); apply add_le_mono_l.
 Qed.
 
-Theorem NZadd_le_mono : forall n m p q : NZ, n <= m -> p <= q -> n + p <= m + q.
+Theorem add_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 -> NZadd_le_mono_r | now apply -> NZadd_le_mono_l].
+apply le_trans with (m + p);
+[now apply -> add_le_mono_r | now apply -> add_le_mono_l].
 Qed.
 
-Theorem NZadd_lt_le_mono : forall n m p q : NZ, n < m -> p <= q -> n + p < m + q.
+Theorem add_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 -> NZadd_lt_mono_r | now apply -> NZadd_le_mono_l].
+apply lt_le_trans with (m + p);
+[now apply -> add_lt_mono_r | now apply -> add_le_mono_l].
 Qed.
 
-Theorem NZadd_le_lt_mono : forall n m p q : NZ, n <= m -> p < q -> n + p < m + q.
+Theorem add_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 -> NZadd_le_mono_r | now apply -> NZadd_lt_mono_l].
+apply le_lt_trans with (m + p);
+[now apply -> add_le_mono_r | now apply -> add_lt_mono_l].
 Qed.
 
-Theorem NZadd_pos_pos : forall n m : NZ, 0 < n -> 0 < m -> 0 < n + m.
+Theorem add_pos_pos : forall n m, 0 < n -> 0 < m -> 0 < n + m.
 Proof.
-intros n m H1 H2. rewrite <- (NZadd_0_l 0). now apply NZadd_lt_mono.
+intros n m H1 H2. rewrite <- (add_0_l 0). now apply add_lt_mono.
 Qed.
 
-Theorem NZadd_pos_nonneg : forall n m : NZ, 0 < n -> 0 <= m -> 0 < n + m.
+Theorem add_pos_nonneg : forall n m, 0 < n -> 0 <= m -> 0 < n + m.
 Proof.
-intros n m H1 H2. rewrite <- (NZadd_0_l 0). now apply NZadd_lt_le_mono.
+intros n m H1 H2. rewrite <- (add_0_l 0). now apply add_lt_le_mono.
 Qed.
 
-Theorem NZadd_nonneg_pos : forall n m : NZ, 0 <= n -> 0 < m -> 0 < n + m.
+Theorem add_nonneg_pos : forall n m, 0 <= n -> 0 < m -> 0 < n + m.
 Proof.
-intros n m H1 H2. rewrite <- (NZadd_0_l 0). now apply NZadd_le_lt_mono.
+intros n m H1 H2. rewrite <- (add_0_l 0). now apply add_le_lt_mono.
 Qed.
 
-Theorem NZadd_nonneg_nonneg : forall n m : NZ, 0 <= n -> 0 <= m -> 0 <= n + m.
+Theorem add_nonneg_nonneg : forall n m, 0 <= n -> 0 <= m -> 0 <= n + m.
 Proof.
-intros n m H1 H2. rewrite <- (NZadd_0_l 0). now apply NZadd_le_mono.
+intros n m H1 H2. rewrite <- (add_0_l 0). now apply add_le_mono.
 Qed.
 
-Theorem NZlt_add_pos_l : forall n m : NZ, 0 < n -> m < n + m.
+Theorem lt_add_pos_l : forall n m, 0 < n -> m < n + m.
 Proof.
-intros n m H. apply -> (NZadd_lt_mono_r 0 n m) in H.
-now rewrite NZadd_0_l in H.
+intros n m. rewrite (add_lt_mono_r 0 n m). now nzsimpl.
 Qed.
 
-Theorem NZlt_add_pos_r : forall n m : NZ, 0 < n -> m < m + n.
+Theorem lt_add_pos_r : forall n m, 0 < n -> m < m + n.
 Proof.
-intros; rewrite NZadd_comm; now apply NZlt_add_pos_l.
+intros; rewrite add_comm; now apply lt_add_pos_l.
 Qed.
 
-Theorem NZle_lt_add_lt : forall n m p q : NZ, n <= m -> p + m < q + n -> p < q.
+Theorem le_lt_add_lt : forall n m p q, n <= m -> p + m < q + n -> p < q.
 Proof.
-intros n m p q H1 H2. destruct (NZle_gt_cases q p); [| assumption].
-pose proof (NZadd_le_mono q p n m H H1) as H3. apply <- NZnle_gt in H2.
-false_hyp H3 H2.
+intros n m p q H1 H2. destruct (le_gt_cases q p); [| assumption].
+contradict H2. rewrite nlt_ge. now apply add_le_mono.
 Qed.
 
-Theorem NZlt_le_add_lt : forall n m p q : NZ, n < m -> p + m <= q + n -> p < q.
+Theorem lt_le_add_lt : forall n m p q, n < m -> p + m <= q + n -> p < q.
 Proof.
-intros n m p q H1 H2. destruct (NZle_gt_cases q p); [| assumption].
-pose proof (NZadd_le_lt_mono q p n m H H1) as H3. apply <- NZnle_gt in H3.
-false_hyp H2 H3.
+intros n m p q H1 H2. destruct (le_gt_cases q p); [| assumption].
+contradict H2. rewrite nle_gt. now apply add_le_lt_mono.
 Qed.
 
-Theorem NZle_le_add_le : forall n m p q : NZ, n <= m -> p + m <= q + n -> p <= q.
+Theorem le_le_add_le : forall n m p q, 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 (NZadd_lt_le_mono q p n m H H1) as H3. apply <- NZnle_gt in H3.
-false_hyp H2 H3.
+intros n m p q H1 H2. destruct (le_gt_cases p q); [assumption |].
+contradict H2. rewrite nle_gt. now apply add_lt_le_mono.
 Qed.
 
-Theorem NZadd_lt_cases : forall n m p q : NZ, n + m < p + q -> n < p \/ m < q.
+Theorem add_lt_cases : forall n m p q, n + m < p + q -> n < p \/ m < q.
 Proof.
 intros n m p q H;
-destruct (NZle_gt_cases p n) as [H1 | H1].
-destruct (NZle_gt_cases q m) as [H2 | H2].
-pose proof (NZadd_le_mono p n q m H1 H2) as H3. apply -> NZle_ngt in H3.
-false_hyp H H3.
-now right. now left.
+destruct (le_gt_cases p n) as [H1 | H1]; [| now left].
+destruct (le_gt_cases q m) as [H2 | H2]; [| now right].
+contradict H; rewrite nlt_ge. now apply add_le_mono.
 Qed.
 
-Theorem NZadd_le_cases : forall n m p q : NZ, n + m <= p + q -> n <= p \/ m <= q.
+Theorem add_le_cases : forall n m p q, n + m <= p + q -> n <= p \/ m <= q.
 Proof.
 intros n m p q H.
-destruct (NZle_gt_cases n p) as [H1 | H1]. now left.
-destruct (NZle_gt_cases m q) as [H2 | H2]. now right.
-assert (H3 : p + q < n + m) by now apply NZadd_lt_mono.
-apply -> NZle_ngt in H. false_hyp H3 H.
+destruct (le_gt_cases n p) as [H1 | H1]. now left.
+destruct (le_gt_cases m q) as [H2 | H2]. now right.
+contradict H; rewrite nle_gt. now apply add_lt_mono.
 Qed.
 
-Theorem NZadd_neg_cases : forall n m : NZ, n + m < 0 -> n < 0 \/ m < 0.
+Theorem add_neg_cases : forall n m, n + m < 0 -> n < 0 \/ m < 0.
 Proof.
-intros n m H; apply NZadd_lt_cases; now rewrite NZadd_0_l.
+intros n m H; apply add_lt_cases; now nzsimpl.
 Qed.
 
-Theorem NZadd_pos_cases : forall n m : NZ, 0 < n + m -> 0 < n \/ 0 < m.
+Theorem add_pos_cases : forall n m, 0 < n + m -> 0 < n \/ 0 < m.
 Proof.
-intros n m H; apply NZadd_lt_cases; now rewrite NZadd_0_l.
+intros n m H; apply add_lt_cases; now nzsimpl.
 Qed.
 
-Theorem NZadd_nonpos_cases : forall n m : NZ, n + m <= 0 -> n <= 0 \/ m <= 0.
+Theorem add_nonpos_cases : forall n m, n + m <= 0 -> n <= 0 \/ m <= 0.
 Proof.
-intros n m H; apply NZadd_le_cases; now rewrite NZadd_0_l.
+intros n m H; apply add_le_cases; now nzsimpl.
 Qed.
 
-Theorem NZadd_nonneg_cases : forall n m : NZ, 0 <= n + m -> 0 <= n \/ 0 <= m.
+Theorem add_nonneg_cases : forall n m, 0 <= n + m -> 0 <= n \/ 0 <= m.
 Proof.
-intros n m H; apply NZadd_le_cases; now rewrite NZadd_0_l.
+intros n m H; apply add_le_cases; now nzsimpl.
 Qed.
 
 End NZAddOrderPropFunct.
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index 8499054b5d..9dd6eaf05d 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -14,80 +14,79 @@ Require Export NumPrelude.
 
 Module Type NZAxiomsSig.
 
-Parameter Inline NZ : Type.
-Parameter Inline NZeq : NZ -> NZ -> Prop.
-Parameter Inline NZ0 : NZ.
-Parameter Inline NZsucc : NZ -> NZ.
-Parameter Inline NZpred : NZ -> NZ.
-Parameter Inline NZadd : NZ -> NZ -> NZ.
-Parameter Inline NZsub : NZ -> NZ -> NZ.
-Parameter Inline NZmul : NZ -> NZ -> NZ.
+Parameter Inline t : Type.
+Parameter Inline eq : t -> t -> Prop.
+Parameter Inline zero : t.
+Parameter Inline succ : t -> t.
+Parameter Inline pred : t -> t.
+Parameter Inline add : t -> t -> t.
+Parameter Inline sub : t -> t -> t.
+Parameter Inline mul : t -> t -> t.
 
 (* Unary subtraction (opp) is not defined on natural numbers, so we have
    it for integers only *)
 
-Instance NZeq_equiv : Equivalence NZeq.
-Instance NZsucc_wd : Proper (NZeq ==> NZeq) NZsucc.
-Instance NZpred_wd : Proper (NZeq ==> NZeq) NZpred.
-Instance NZadd_wd : Proper (NZeq ==> NZeq ==> NZeq) NZadd.
-Instance NZsub_wd : Proper (NZeq ==> NZeq ==> NZeq) NZsub.
-Instance NZmul_wd : Proper (NZeq ==> NZeq ==> NZeq) NZmul.
+Instance eq_equiv : Equivalence eq.
+Instance succ_wd : Proper (eq ==> eq) succ.
+Instance pred_wd : Proper (eq ==> eq) pred.
+Instance add_wd : Proper (eq ==> eq ==> eq) add.
+Instance sub_wd : Proper (eq ==> eq ==> eq) sub.
+Instance mul_wd : Proper (eq ==> eq ==> eq) mul.
 
-Delimit Scope NatIntScope with NatInt.
-Open Local Scope NatIntScope.
-Notation "x == y"  := (NZeq x y) (at level 70) : NatIntScope.
-Notation "x ~= y" := (~ NZeq x y) (at level 70) : NatIntScope.
-Notation "0" := NZ0 : NatIntScope.
-Notation S := NZsucc.
-Notation P := NZpred.
-Notation "1" := (S 0) : NatIntScope.
-Notation "x + y" := (NZadd x y) : NatIntScope.
-Notation "x - y" := (NZsub x y) : NatIntScope.
-Notation "x * y" := (NZmul x y) : NatIntScope.
+Delimit Scope NumScope with Num.
+Local Open Scope NumScope.
+Notation "x == y"  := (eq x y) (at level 70) : NumScope.
+Notation "x ~= y" := (~ eq x y) (at level 70) : NumScope.
+Notation "0" := zero : NumScope.
+Notation S := succ.
+Notation P := pred.
+Notation "1" := (S 0) : NumScope.
+Notation "x + y" := (add x y) : NumScope.
+Notation "x - y" := (sub x y) : NumScope.
+Notation "x * y" := (mul x y) : NumScope.
 
-Axiom NZpred_succ : forall n : NZ, P (S n) == n.
+Axiom pred_succ : forall n, P (S n) == n.
 
-Axiom NZinduction :
-  forall A : NZ -> Prop, Proper (NZeq==>iff) A ->
-    A 0 -> (forall n : NZ, A n <-> A (S n)) -> forall n : NZ, A n.
+Axiom bi_induction :
+  forall A : t -> Prop, Proper (eq==>iff) A ->
+    A 0 -> (forall n, A n <-> A (S n)) -> forall n, A n.
 
-Axiom NZadd_0_l : forall n : NZ, 0 + n == n.
-Axiom NZadd_succ_l : forall n m : NZ, (S n) + m == S (n + m).
+Axiom add_0_l : forall n, 0 + n == n.
+Axiom add_succ_l : forall n m, (S n) + m == S (n + m).
 
-Axiom NZsub_0_r : forall n : NZ, n - 0 == n.
-Axiom NZsub_succ_r : forall n m : NZ, n - (S m) == P (n - m).
+Axiom sub_0_r : forall n, n - 0 == n.
+Axiom sub_succ_r : forall n m, n - (S m) == P (n - m).
 
-Axiom NZmul_0_l : forall n : NZ, 0 * n == 0.
-Axiom NZmul_succ_l : forall n m : NZ, S n * m == n * m + m.
+Axiom mul_0_l : forall n, 0 * n == 0.
+Axiom mul_succ_l : forall n m, S n * m == n * m + m.
 
 End NZAxiomsSig.
 
 Module Type NZOrdAxiomsSig.
-Declare Module Export NZAxiomsMod : NZAxiomsSig.
-Open Local Scope NatIntScope.
-
-Parameter Inline NZlt : NZ -> NZ -> Prop.
-Parameter Inline NZle : NZ -> NZ -> Prop.
-Parameter Inline NZmin : NZ -> NZ -> NZ.
-Parameter Inline NZmax : NZ -> NZ -> NZ.
-
-Instance NZlt_wd : Proper (NZeq ==> NZeq ==> iff) NZlt.
-Instance NZle_wd : Proper (NZeq ==> NZeq ==> iff) NZle.
-Instance NZmin_wd : Proper (NZeq ==> NZeq ==> NZeq) NZmin.
-Instance NZmax_wd : Proper (NZeq ==> NZeq ==> NZeq) NZmax.
-
-Notation "x < y" := (NZlt x y) : NatIntScope.
-Notation "x <= y" := (NZle x y) : NatIntScope.
-Notation "x > y" := (NZlt y x) (only parsing) : NatIntScope.
-Notation "x >= y" := (NZle y x) (only parsing) : NatIntScope.
-
-Axiom NZlt_eq_cases : forall n m : NZ, n <= m <-> n < m \/ n == m.
-Axiom NZlt_irrefl : forall n : NZ, ~ (n < n).
-Axiom NZlt_succ_r : forall n m : NZ, n < S m <-> n <= m.
-
-Axiom NZmin_l : forall n m : NZ, n <= m -> NZmin n m == n.
-Axiom NZmin_r : forall n m : NZ, m <= n -> NZmin n m == m.
-Axiom NZmax_l : forall n m : NZ, m <= n -> NZmax n m == n.
-Axiom NZmax_r : forall n m : NZ, n <= m -> NZmax n m == m.
+Include Type NZAxiomsSig.
+Local Open Scope NumScope.
+
+Parameter Inline lt : t -> t -> Prop.
+Parameter Inline le : t -> t -> Prop.
+
+Notation "x < y" := (lt x y) : NumScope.
+Notation "x <= y" := (le x y) : NumScope.
+Notation "x > y" := (lt y x) (only parsing) : NumScope.
+Notation "x >= y" := (le y x) (only parsing) : NumScope.
+
+Instance lt_wd : Proper (eq ==> eq ==> iff) lt.
+(** Compatibility of [le] can be proved later from [lt_wd] and [lt_eq_cases] *)
+
+Axiom lt_eq_cases : forall n m, n <= m <-> n < m \/ n == m.
+Axiom lt_irrefl : forall n, ~ (n < n).
+Axiom lt_succ_r : forall n m, n < S m <-> n <= m.
+
+Parameter Inline min : t -> t -> t.
+Parameter Inline max : t -> t -> t.
+(** Compatibility of [min] and [max] can be proved later *)
+Axiom min_l : forall n m, n <= m -> min n m == n.
+Axiom min_r : forall n m, m <= n -> min n m == m.
+Axiom max_l : forall n m, m <= n -> max n m == n.
+Axiom max_r : forall n m, n <= m -> max n m == m.
 
 End NZOrdAxiomsSig.
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 0c9d006d68..b958245652 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -12,41 +12,48 @@
 
 Require Import NZAxioms.
 
-Module NZBasePropFunct (Import NZAxiomsMod : NZAxiomsSig).
-Open Local Scope NatIntScope.
+Module NZBasePropFunct (Import NZ : NZAxiomsSig).
+Local Open Scope NumScope.
 
-Theorem NZneq_sym : forall n m : NZ, n ~= m -> m ~= n.
+Definition eq_refl := @Equivalence_Reflexive _ _ eq_equiv.
+Definition eq_sym := @Equivalence_Symmetric _ _ eq_equiv.
+Definition eq_trans := @Equivalence_Transitive _ _ eq_equiv.
+
+(* TODO: how register ~= (which is just a notation) as a Symmetric relation,
+    hence allowing "symmetry" tac ? *)
+
+Theorem neq_sym : forall n m, n ~= m -> m ~= n.
 Proof.
 intros n m H1 H2; symmetry in H2; false_hyp H2 H1.
 Qed.
 
-Theorem NZE_stepl : forall x y z : NZ, x == y -> x == z -> z == y.
+Theorem eq_stepl : forall x y z, x == y -> x == z -> z == y.
 Proof.
 intros x y z H1 H2; now rewrite <- H1.
 Qed.
 
-Declare Left Step NZE_stepl.
-(* The right step lemma is just the transitivity of NZeq *)
-Declare Right Step (@Equivalence_Transitive _ _ NZeq_equiv).
+Declare Left Step eq_stepl.
+(* The right step lemma is just the transitivity of eq *)
+Declare Right Step (@Equivalence_Transitive _ _ eq_equiv).
 
-Theorem NZsucc_inj : forall n1 n2 : NZ, S n1 == S n2 -> n1 == n2.
+Theorem succ_inj : forall n1 n2, S n1 == S n2 -> n1 == n2.
 Proof.
 intros n1 n2 H.
-apply NZpred_wd in H. now do 2 rewrite NZpred_succ in H.
+apply pred_wd in H. now do 2 rewrite pred_succ in H.
 Qed.
 
 (* The following theorem is useful as an equivalence for proving
 bidirectional induction steps *)
-Theorem NZsucc_inj_wd : forall n1 n2 : NZ, S n1 == S n2 <-> n1 == n2.
+Theorem succ_inj_wd : forall n1 n2, S n1 == S n2 <-> n1 == n2.
 Proof.
 intros; split.
-apply NZsucc_inj.
-apply NZsucc_wd.
+apply succ_inj.
+apply succ_wd.
 Qed.
 
-Theorem NZsucc_inj_wd_neg : forall n m : NZ, S n ~= S m <-> n ~= m.
+Theorem succ_inj_wd_neg : forall n m, S n ~= S m <-> n ~= m.
 Proof.
-intros; now rewrite NZsucc_inj_wd.
+intros; now rewrite succ_inj_wd.
 Qed.
 
 (* We cannot prove that the predecessor is injective, nor that it is
@@ -54,28 +61,27 @@ left-inverse to the successor at this point *)
 
 Section CentralInduction.
 
-Variable A : predicate NZ.
-
-Hypothesis A_wd : Proper (NZeq==>iff) A.
+Variable A : predicate t.
+Hypothesis A_wd : Proper (eq==>iff) A.
 
-Theorem NZcentral_induction :
-  forall z : NZ, A z ->
-    (forall n : NZ, A n <-> A (S n)) ->
-      forall n : NZ, A n.
+Theorem central_induction :
+  forall z, A z ->
+    (forall n, A n <-> A (S n)) ->
+      forall n, A n.
 Proof.
-intros z Base Step; revert Base; pattern z; apply NZinduction.
+intros z Base Step; revert Base; pattern z; apply bi_induction.
 solve_predicate_wd.
-intro; now apply NZinduction.
+intro; now apply bi_induction.
 intro; pose proof (Step n); tauto.
 Qed.
 
 End CentralInduction.
 
-Tactic Notation "NZinduct" ident(n) :=
-  induction_maker n ltac:(apply NZinduction).
+Tactic Notation "nzinduct" ident(n) :=
+  induction_maker n ltac:(apply bi_induction).
 
-Tactic Notation "NZinduct" ident(n) constr(u) :=
-  induction_maker n ltac:(apply NZcentral_induction with (z := u)).
+Tactic Notation "nzinduct" ident(n) constr(u) :=
+  induction_maker n ltac:(apply central_induction with (z := u)).
 
 End NZBasePropFunct.
 
diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v
index 7d9b1aabd3..c76e25c64c 100644
--- a/theories/Numbers/NatInt/NZMul.v
+++ b/theories/Numbers/NatInt/NZMul.v
@@ -13,67 +13,59 @@
 Require Import NZAxioms.
 Require Import NZAdd.
 
-Module NZMulPropFunct (Import NZAxiomsMod : NZAxiomsSig).
-Module Export NZAddPropMod := NZAddPropFunct NZAxiomsMod.
-Open Local Scope NatIntScope.
+Module NZMulPropFunct (Import NZ : NZAxiomsSig).
+Include NZAddPropFunct NZ.
+Local Open Scope NumScope.
 
-Theorem NZmul_0_r : forall n : NZ, n * 0 == 0.
+Theorem mul_0_r : forall n, n * 0 == 0.
 Proof.
-NZinduct n.
-now rewrite NZmul_0_l.
-intro. rewrite NZmul_succ_l. now rewrite NZadd_0_r.
+nzinduct n; intros; now nzsimpl.
 Qed.
 
-Theorem NZmul_succ_r : forall n m : NZ, n * (S m) == n * m + n.
+Theorem mul_succ_r : forall n m, n * (S m) == n * m + n.
 Proof.
-intros n m; NZinduct n.
-do 2 rewrite NZmul_0_l; now rewrite NZadd_0_l.
-intro n. do 2 rewrite NZmul_succ_l. do 2 rewrite NZadd_succ_r.
-rewrite NZsucc_inj_wd. rewrite <- (NZadd_assoc (n * m) m n).
-rewrite (NZadd_comm m n). rewrite NZadd_assoc.
-now rewrite NZadd_cancel_r.
+intros n m; nzinduct n. now nzsimpl.
+intro n. nzsimpl. rewrite succ_inj_wd, <- add_assoc, (add_comm m n), add_assoc.
+now rewrite add_cancel_r.
 Qed.
 
-Theorem NZmul_comm : forall n m : NZ, n * m == m * n.
+Hint Rewrite mul_0_r mul_succ_r : nz.
+
+Theorem mul_comm : forall n m, n * m == m * n.
 Proof.
-intros n m; NZinduct n.
-rewrite NZmul_0_l; now rewrite NZmul_0_r.
-intro. rewrite NZmul_succ_l; rewrite NZmul_succ_r. now rewrite NZadd_cancel_r.
+intros n m; nzinduct n. now nzsimpl.
+intro. nzsimpl. now rewrite add_cancel_r.
 Qed.
 
-Theorem NZmul_add_distr_r : forall n m p : NZ, (n + m) * p == n * p + m * p.
+Theorem mul_add_distr_r : forall n m p, (n + m) * p == n * p + m * p.
 Proof.
-intros n m p; NZinduct n.
-rewrite NZmul_0_l. now do 2 rewrite NZadd_0_l.
-intro n. rewrite NZadd_succ_l. do 2 rewrite NZmul_succ_l.
-rewrite <- (NZadd_assoc (n * p) p (m * p)).
-rewrite (NZadd_comm p (m * p)). rewrite (NZadd_assoc (n * p) (m * p) p).
-now rewrite NZadd_cancel_r.
+intros n m p; nzinduct n. now nzsimpl.
+intro n. nzsimpl. rewrite <- add_assoc, (add_comm p (m*p)), add_assoc.
+now rewrite add_cancel_r.
 Qed.
 
-Theorem NZmul_add_distr_l : forall n m p : NZ, n * (m + p) == n * m + n * p.
+Theorem mul_add_distr_l : forall n m p, n * (m + p) == n * m + n * p.
 Proof.
 intros n m p.
-rewrite (NZmul_comm n (m + p)). rewrite (NZmul_comm n m).
-rewrite (NZmul_comm n p). apply NZmul_add_distr_r.
+rewrite (mul_comm n (m + p)), (mul_comm n m), (mul_comm n p).
+apply mul_add_distr_r.
 Qed.
 
-Theorem NZmul_assoc : forall n m p : NZ, n * (m * p) == (n * m) * p.
+Theorem mul_assoc : forall n m p, n * (m * p) == (n * m) * p.
 Proof.
-intros n m p; NZinduct n.
-now do 3 rewrite NZmul_0_l.
-intro n. do 2 rewrite NZmul_succ_l. rewrite NZmul_add_distr_r.
-now rewrite NZadd_cancel_r.
+intros n m p; nzinduct n. now nzsimpl.
+intro n. nzsimpl. rewrite mul_add_distr_r.
+now rewrite add_cancel_r.
 Qed.
 
-Theorem NZmul_1_l : forall n : NZ, 1 * n == n.
+Theorem mul_1_l : forall n, 1 * n == n.
 Proof.
-intro n. rewrite NZmul_succ_l; rewrite NZmul_0_l. now rewrite NZadd_0_l.
+intro n. now nzsimpl.
 Qed.
 
-Theorem NZmul_1_r : forall n : NZ, n * 1 == n.
+Theorem mul_1_r : forall n, n * 1 == n.
 Proof.
-intro n; rewrite NZmul_comm; apply NZmul_1_l.
+intro n. now nzsimpl.
 Qed.
 
 End NZMulPropFunct.
diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v
index d6eea61c8c..306b69022c 100644
--- a/theories/Numbers/NatInt/NZMulOrder.v
+++ b/theories/Numbers/NatInt/NZMulOrder.v
@@ -13,298 +13,291 @@
 Require Import NZAxioms.
 Require Import NZAddOrder.
 
-Module NZMulOrderPropFunct (Import NZOrdAxiomsMod : NZOrdAxiomsSig).
-Module Export NZAddOrderPropMod := NZAddOrderPropFunct NZOrdAxiomsMod.
-Open Local Scope NatIntScope.
+Module NZMulOrderPropFunct (Import NZ : NZOrdAxiomsSig).
+Include NZAddOrderPropFunct NZ.
+Local Open Scope NumScope.
 
-Theorem NZmul_lt_pred :
-  forall p q n m : NZ, S p == q -> (p * n < p * m <-> q * n + m < q * m + n).
+Theorem mul_lt_pred :
+  forall p q n m, S p == q -> (p * n < p * m <-> q * n + m < q * m + n).
 Proof.
-intros p q n m H. rewrite <- H. do 2 rewrite NZmul_succ_l.
-rewrite <- (NZadd_assoc (p * n) n m).
-rewrite <- (NZadd_assoc (p * m) m n).
-rewrite (NZadd_comm n m). now rewrite <- NZadd_lt_mono_r.
+intros p q n m H. rewrite <- H. nzsimpl.
+rewrite <- ! add_assoc, (add_comm n m).
+now rewrite <- add_lt_mono_r.
 Qed.
 
-Theorem NZmul_lt_mono_pos_l : forall p n m : NZ, 0 < p -> (n < m <-> p * n < p * m).
+Theorem mul_lt_mono_pos_l : forall p n m, 0 < p -> (n < m <-> p * n < p * m).
 Proof.
-NZord_induct p.
-intros n m H; false_hyp H NZlt_irrefl.
-intros p H IH n m H1. do 2 rewrite NZmul_succ_l.
-le_elim H. assert (LR : forall n m : NZ, n < m -> p * n + n < p * m + m).
-intros n1 m1 H2. apply NZadd_lt_mono; [now apply -> IH | assumption].
-split; [apply LR |]. intro H2. apply -> NZlt_dne; intro H3.
-apply <- NZle_ngt in H3. le_elim H3.
-apply NZlt_asymm in H2. apply H2. now apply LR.
-rewrite H3 in H2; false_hyp H2 NZlt_irrefl.
-rewrite <- H; do 2 rewrite NZmul_0_l; now do 2 rewrite NZadd_0_l.
-intros p H1 _ n m H2. apply NZlt_asymm in H1. false_hyp H2 H1.
+nzord_induct p.
+intros n m H; false_hyp H lt_irrefl.
+intros p H IH n m H1. nzsimpl.
+le_elim H. assert (LR : forall n m, n < m -> p * n + n < p * m + m).
+intros n1 m1 H2. apply add_lt_mono; [now apply -> IH | assumption].
+split; [apply LR |]. intro H2. apply -> lt_dne; intro H3.
+apply <- le_ngt in H3. le_elim H3.
+apply lt_asymm in H2. apply H2. now apply LR.
+rewrite H3 in H2; false_hyp H2 lt_irrefl.
+rewrite <- H; now nzsimpl.
+intros p H1 _ n m H2. destruct (lt_asymm _ _ H1 H2).
 Qed.
 
-Theorem NZmul_lt_mono_pos_r : forall p n m : NZ, 0 < p -> (n < m <-> n * p < m * p).
+Theorem mul_lt_mono_pos_r : forall p n m, 0 < p -> (n < m <-> n * p < m * p).
 Proof.
 intros p n m.
-rewrite (NZmul_comm n p); rewrite (NZmul_comm m p). now apply NZmul_lt_mono_pos_l.
+rewrite (mul_comm n p), (mul_comm m p). now apply mul_lt_mono_pos_l.
 Qed.
 
-Theorem NZmul_lt_mono_neg_l : forall p n m : NZ, p < 0 -> (n < m <-> p * m < p * n).
+Theorem mul_lt_mono_neg_l : forall p n m, p < 0 -> (n < m <-> p * m < p * n).
 Proof.
-NZord_induct p.
-intros n m H; false_hyp H NZlt_irrefl.
-intros p H1 _ n m H2. apply NZlt_succ_l in H2. apply <- NZnle_gt in H2. false_hyp H1 H2.
-intros p H IH n m H1. apply <- NZle_succ_l in H.
-le_elim H. assert (LR : forall n m : NZ, n < m -> p * m < p * n).
-intros n1 m1 H2. apply (NZle_lt_add_lt n1 m1).
-now apply NZlt_le_incl. do 2 rewrite <- NZmul_succ_l. now apply -> IH.
-split; [apply LR |]. intro H2. apply -> NZlt_dne; intro H3.
-apply <- NZle_ngt in H3. le_elim H3.
-apply NZlt_asymm in H2. apply H2. now apply LR.
-rewrite H3 in H2; false_hyp H2 NZlt_irrefl.
-rewrite (NZmul_lt_pred p (S p)) by reflexivity.
-rewrite H; do 2 rewrite NZmul_0_l; now do 2 rewrite NZadd_0_l.
+nzord_induct p.
+intros n m H; false_hyp H lt_irrefl.
+intros p H1 _ n m H2. apply lt_succ_l in H2. apply <- nle_gt in H2.
+false_hyp H1 H2.
+intros p H IH n m H1. apply <- le_succ_l in H.
+le_elim H. assert (LR : forall n m, n < m -> p * m < p * n).
+intros n1 m1 H2. apply (le_lt_add_lt n1 m1).
+now apply lt_le_incl. rewrite <- 2 mul_succ_l. now apply -> IH.
+split; [apply LR |]. intro H2. apply -> lt_dne; intro H3.
+apply <- le_ngt in H3. le_elim H3.
+apply lt_asymm in H2. apply H2. now apply LR.
+rewrite H3 in H2; false_hyp H2 lt_irrefl.
+rewrite (mul_lt_pred p (S p)) by reflexivity.
+rewrite H; do 2 rewrite mul_0_l; now do 2 rewrite add_0_l.
 Qed.
 
-Theorem NZmul_lt_mono_neg_r : forall p n m : NZ, p < 0 -> (n < m <-> m * p < n * p).
+Theorem mul_lt_mono_neg_r : forall p n m, p < 0 -> (n < m <-> m * p < n * p).
 Proof.
 intros p n m.
-rewrite (NZmul_comm n p); rewrite (NZmul_comm m p). now apply NZmul_lt_mono_neg_l.
+rewrite (mul_comm n p), (mul_comm m p). now apply mul_lt_mono_neg_l.
 Qed.
 
-Theorem NZmul_le_mono_nonneg_l : forall n m p : NZ, 0 <= p -> n <= m -> p * n <= p * m.
+Theorem mul_le_mono_nonneg_l : forall n m p, 0 <= p -> n <= m -> p * n <= p * m.
 Proof.
 intros n m p H1 H2. le_elim H1.
-le_elim H2. apply NZlt_le_incl. now apply -> NZmul_lt_mono_pos_l.
-apply NZeq_le_incl; now rewrite H2.
-apply NZeq_le_incl; rewrite <- H1; now do 2 rewrite NZmul_0_l.
+le_elim H2. apply lt_le_incl. now apply -> mul_lt_mono_pos_l.
+apply eq_le_incl; now rewrite H2.
+apply eq_le_incl; rewrite <- H1; now do 2 rewrite mul_0_l.
 Qed.
 
-Theorem NZmul_le_mono_nonpos_l : forall n m p : NZ, p <= 0 -> n <= m -> p * m <= p * n.
+Theorem mul_le_mono_nonpos_l : forall n m p, p <= 0 -> n <= m -> p * m <= p * n.
 Proof.
 intros n m p H1 H2. le_elim H1.
-le_elim H2. apply NZlt_le_incl. now apply -> NZmul_lt_mono_neg_l.
-apply NZeq_le_incl; now rewrite H2.
-apply NZeq_le_incl; rewrite H1; now do 2 rewrite NZmul_0_l.
+le_elim H2. apply lt_le_incl. now apply -> mul_lt_mono_neg_l.
+apply eq_le_incl; now rewrite H2.
+apply eq_le_incl; rewrite H1; now do 2 rewrite mul_0_l.
 Qed.
 
-Theorem NZmul_le_mono_nonneg_r : forall n m p : NZ, 0 <= p -> n <= m -> n * p <= m * p.
+Theorem mul_le_mono_nonneg_r : forall n m p, 0 <= p -> n <= m -> n * p <= m * p.
 Proof.
-intros n m p H1 H2; rewrite (NZmul_comm n p); rewrite (NZmul_comm m p);
-now apply NZmul_le_mono_nonneg_l.
+intros n m p H1 H2;
+rewrite (mul_comm n p), (mul_comm m p); now apply mul_le_mono_nonneg_l.
 Qed.
 
-Theorem NZmul_le_mono_nonpos_r : forall n m p : NZ, p <= 0 -> n <= m -> m * p <= n * p.
+Theorem mul_le_mono_nonpos_r : forall n m p, p <= 0 -> n <= m -> m * p <= n * p.
 Proof.
-intros n m p H1 H2; rewrite (NZmul_comm n p); rewrite (NZmul_comm m p);
-now apply NZmul_le_mono_nonpos_l.
+intros n m p H1 H2;
+rewrite (mul_comm n p), (mul_comm m p); now apply mul_le_mono_nonpos_l.
 Qed.
 
-Theorem NZmul_cancel_l : forall n m p : NZ, p ~= 0 -> (p * n == p * m <-> n == m).
+Theorem mul_cancel_l : forall n m p, p ~= 0 -> (p * n == p * m <-> n == m).
 Proof.
 intros n m p H; split; intro H1.
-destruct (NZlt_trichotomy p 0) as [H2 | [H2 | H2]].
-apply -> NZeq_dne; intro H3. apply -> NZlt_gt_cases in H3. destruct H3 as [H3 | H3].
-assert (H4 : p * m < p * n); [now apply -> NZmul_lt_mono_neg_l |].
-rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
-assert (H4 : p * n < p * m); [now apply -> NZmul_lt_mono_neg_l |].
-rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
+destruct (lt_trichotomy p 0) as [H2 | [H2 | H2]].
+apply -> eq_dne; intro H3. apply -> lt_gt_cases in H3. destruct H3 as [H3 | H3].
+assert (H4 : p * m < p * n); [now apply -> mul_lt_mono_neg_l |].
+rewrite H1 in H4; false_hyp H4 lt_irrefl.
+assert (H4 : p * n < p * m); [now apply -> mul_lt_mono_neg_l |].
+rewrite H1 in H4; false_hyp H4 lt_irrefl.
 false_hyp H2 H.
-apply -> NZeq_dne; intro H3. apply -> NZlt_gt_cases in H3. destruct H3 as [H3 | H3].
-assert (H4 : p * n < p * m) by (now apply -> NZmul_lt_mono_pos_l).
-rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
-assert (H4 : p * m < p * n) by (now apply -> NZmul_lt_mono_pos_l).
-rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
+apply -> eq_dne; intro H3. apply -> lt_gt_cases in H3. destruct H3 as [H3 | H3].
+assert (H4 : p * n < p * m) by (now apply -> mul_lt_mono_pos_l).
+rewrite H1 in H4; false_hyp H4 lt_irrefl.
+assert (H4 : p * m < p * n) by (now apply -> mul_lt_mono_pos_l).
+rewrite H1 in H4; false_hyp H4 lt_irrefl.
 now rewrite H1.
 Qed.
 
-Theorem NZmul_cancel_r : forall n m p : NZ, p ~= 0 -> (n * p == m * p <-> n == m).
+Theorem mul_cancel_r : forall n m p, p ~= 0 -> (n * p == m * p <-> n == m).
 Proof.
-intros n m p. rewrite (NZmul_comm n p), (NZmul_comm m p); apply NZmul_cancel_l.
+intros n m p. rewrite (mul_comm n p), (mul_comm m p); apply mul_cancel_l.
 Qed.
 
-Theorem NZmul_id_l : forall n m : NZ, m ~= 0 -> (n * m == m <-> n == 1).
+Theorem mul_id_l : forall n m, m ~= 0 -> (n * m == m <-> n == 1).
 Proof.
 intros n m H.
-stepl (n * m == 1 * m) by now rewrite NZmul_1_l. now apply NZmul_cancel_r.
+stepl (n * m == 1 * m) by now rewrite mul_1_l. now apply mul_cancel_r.
 Qed.
 
-Theorem NZmul_id_r : forall n m : NZ, n ~= 0 -> (n * m == n <-> m == 1).
+Theorem mul_id_r : forall n m, n ~= 0 -> (n * m == n <-> m == 1).
 Proof.
-intros n m; rewrite NZmul_comm; apply NZmul_id_l.
+intros n m; rewrite mul_comm; apply mul_id_l.
 Qed.
 
-Theorem NZmul_le_mono_pos_l : forall n m p : NZ, 0 < p -> (n <= m <-> p * n <= p * m).
+Theorem mul_le_mono_pos_l : forall n m p, 0 < p -> (n <= m <-> p * n <= p * m).
 Proof.
-intros n m p H; do 2 rewrite NZlt_eq_cases.
-rewrite (NZmul_lt_mono_pos_l p n m) by assumption.
-now rewrite -> (NZmul_cancel_l n m p) by
-(intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl).
+intros n m p H; do 2 rewrite lt_eq_cases.
+rewrite (mul_lt_mono_pos_l p n m) by assumption.
+now rewrite -> (mul_cancel_l n m p) by
+(intro H1; rewrite H1 in H; false_hyp H lt_irrefl).
 Qed.
 
-Theorem NZmul_le_mono_pos_r : forall n m p : NZ, 0 < p -> (n <= m <-> n * p <= m * p).
+Theorem mul_le_mono_pos_r : forall n m p, 0 < p -> (n <= m <-> n * p <= m * p).
 Proof.
-intros n m p. rewrite (NZmul_comm n p); rewrite (NZmul_comm m p);
-apply NZmul_le_mono_pos_l.
+intros n m p. rewrite (mul_comm n p), (mul_comm m p); apply mul_le_mono_pos_l.
 Qed.
 
-Theorem NZmul_le_mono_neg_l : forall n m p : NZ, p < 0 -> (n <= m <-> p * m <= p * n).
+Theorem mul_le_mono_neg_l : forall n m p, p < 0 -> (n <= m <-> p * m <= p * n).
 Proof.
-intros n m p H; do 2 rewrite NZlt_eq_cases.
-rewrite (NZmul_lt_mono_neg_l p n m); [| assumption].
-rewrite -> (NZmul_cancel_l m n p) by (intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl).
-now setoid_replace (n == m) with (m == n) using relation iff by (split; now intro).
+intros n m p H; do 2 rewrite lt_eq_cases.
+rewrite (mul_lt_mono_neg_l p n m); [| assumption].
+rewrite -> (mul_cancel_l m n p)
+ by (intro H1; rewrite H1 in H; false_hyp H lt_irrefl).
+now setoid_replace (n == m) with (m == n) by (split; now intro).
 Qed.
 
-Theorem NZmul_le_mono_neg_r : forall n m p : NZ, p < 0 -> (n <= m <-> m * p <= n * p).
+Theorem mul_le_mono_neg_r : forall n m p, p < 0 -> (n <= m <-> m * p <= n * p).
 Proof.
-intros n m p. rewrite (NZmul_comm n p); rewrite (NZmul_comm m p);
-apply NZmul_le_mono_neg_l.
+intros n m p. rewrite (mul_comm n p), (mul_comm m p); apply mul_le_mono_neg_l.
 Qed.
 
-Theorem NZmul_lt_mono_nonneg :
-  forall n m p q : NZ, 0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q.
+Theorem mul_lt_mono_nonneg :
+  forall n m p q, 0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q.
 Proof.
 intros n m p q H1 H2 H3 H4.
-apply NZle_lt_trans with (m * p).
-apply NZmul_le_mono_nonneg_r; [assumption | now apply NZlt_le_incl].
-apply -> NZmul_lt_mono_pos_l; [assumption | now apply NZle_lt_trans with n].
+apply le_lt_trans with (m * p).
+apply mul_le_mono_nonneg_r; [assumption | now apply lt_le_incl].
+apply -> mul_lt_mono_pos_l; [assumption | now apply le_lt_trans with n].
 Qed.
 
 (* There are still many variants of the theorem above. One can assume 0 < n
 or 0 < p or n <= m or p <= q. *)
 
-Theorem NZmul_le_mono_nonneg :
-  forall n m p q : NZ, 0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q.
+Theorem mul_le_mono_nonneg :
+  forall n m p q, 0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q.
 Proof.
 intros n m p q H1 H2 H3 H4.
 le_elim H2; le_elim H4.
-apply NZlt_le_incl; now apply NZmul_lt_mono_nonneg.
-rewrite <- H4; apply NZmul_le_mono_nonneg_r; [assumption | now apply NZlt_le_incl].
-rewrite <- H2; apply NZmul_le_mono_nonneg_l; [assumption | now apply NZlt_le_incl].
-rewrite H2; rewrite H4; now apply NZeq_le_incl.
+apply lt_le_incl; now apply mul_lt_mono_nonneg.
+rewrite <- H4; apply mul_le_mono_nonneg_r; [assumption | now apply lt_le_incl].
+rewrite <- H2; apply mul_le_mono_nonneg_l; [assumption | now apply lt_le_incl].
+rewrite H2; rewrite H4; now apply eq_le_incl.
 Qed.
 
-Theorem NZmul_pos_pos : forall n m : NZ, 0 < n -> 0 < m -> 0 < n * m.
+Theorem mul_pos_pos : forall n m, 0 < n -> 0 < m -> 0 < n * m.
 Proof.
-intros n m H1 H2.
-rewrite <- (NZmul_0_l m). now apply -> NZmul_lt_mono_pos_r.
+intros n m H1 H2. rewrite <- (mul_0_l m). now apply -> mul_lt_mono_pos_r.
 Qed.
 
-Theorem NZmul_neg_neg : forall n m : NZ, n < 0 -> m < 0 -> 0 < n * m.
+Theorem mul_neg_neg : forall n m, n < 0 -> m < 0 -> 0 < n * m.
 Proof.
-intros n m H1 H2.
-rewrite <- (NZmul_0_l m). now apply -> NZmul_lt_mono_neg_r.
+intros n m H1 H2. rewrite <- (mul_0_l m). now apply -> mul_lt_mono_neg_r.
 Qed.
 
-Theorem NZmul_pos_neg : forall n m : NZ, 0 < n -> m < 0 -> n * m < 0.
+Theorem mul_pos_neg : forall n m, 0 < n -> m < 0 -> n * m < 0.
 Proof.
-intros n m H1 H2.
-rewrite <- (NZmul_0_l m). now apply -> NZmul_lt_mono_neg_r.
+intros n m H1 H2. rewrite <- (mul_0_l m). now apply -> mul_lt_mono_neg_r.
 Qed.
 
-Theorem NZmul_neg_pos : forall n m : NZ, n < 0 -> 0 < m -> n * m < 0.
+Theorem mul_neg_pos : forall n m, n < 0 -> 0 < m -> n * m < 0.
 Proof.
-intros; rewrite NZmul_comm; now apply NZmul_pos_neg.
+intros; rewrite mul_comm; now apply mul_pos_neg.
 Qed.
 
-Theorem NZlt_1_mul_pos : forall n m : NZ, 1 < n -> 0 < m -> 1 < n * m.
+Theorem lt_1_mul_pos : forall n m, 1 < n -> 0 < m -> 1 < n * m.
 Proof.
-intros n m H1 H2. apply -> (NZmul_lt_mono_pos_r m) in H1.
-rewrite NZmul_1_l in H1. now apply NZlt_1_l with m.
+intros n m H1 H2. apply -> (mul_lt_mono_pos_r m) in H1.
+rewrite mul_1_l in H1. now apply lt_1_l with m.
 assumption.
 Qed.
 
-Theorem NZeq_mul_0 : forall n m : NZ, n * m == 0 <-> n == 0 \/ m == 0.
+Theorem eq_mul_0 : forall n m, n * m == 0 <-> n == 0 \/ m == 0.
 Proof.
 intros n m; split.
-intro H; destruct (NZlt_trichotomy n 0) as [H1 | [H1 | H1]];
-destruct (NZlt_trichotomy m 0) as [H2 | [H2 | H2]];
+intro H; destruct (lt_trichotomy n 0) as [H1 | [H1 | H1]];
+destruct (lt_trichotomy m 0) as [H2 | [H2 | H2]];
 try (now right); try (now left).
-exfalso; now apply (NZlt_neq 0 (n * m)); [apply NZmul_neg_neg |].
-exfalso; now apply (NZlt_neq (n * m) 0); [apply NZmul_neg_pos |].
-exfalso; now apply (NZlt_neq (n * m) 0); [apply NZmul_pos_neg |].
-exfalso; now apply (NZlt_neq 0 (n * m)); [apply NZmul_pos_pos |].
-intros [H | H]. now rewrite H, NZmul_0_l. now rewrite H, NZmul_0_r.
+exfalso; now apply (lt_neq 0 (n * m)); [apply mul_neg_neg |].
+exfalso; now apply (lt_neq (n * m) 0); [apply mul_neg_pos |].
+exfalso; now apply (lt_neq (n * m) 0); [apply mul_pos_neg |].
+exfalso; now apply (lt_neq 0 (n * m)); [apply mul_pos_pos |].
+intros [H | H]. now rewrite H, mul_0_l. now rewrite H, mul_0_r.
 Qed.
 
-Theorem NZneq_mul_0 : forall n m : NZ, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
+Theorem neq_mul_0 : forall n m, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
 Proof.
 intros n m; split; intro H.
-intro H1; apply -> NZeq_mul_0 in H1. tauto.
+intro H1; apply -> eq_mul_0 in H1. tauto.
 split; intro H1; rewrite H1 in H;
-(rewrite NZmul_0_l in H || rewrite NZmul_0_r in H); now apply H.
+(rewrite mul_0_l in H || rewrite mul_0_r in H); now apply H.
 Qed.
 
-Theorem NZeq_square_0 : forall n : NZ, n * n == 0 <-> n == 0.
+Theorem eq_square_0 : forall n, n * n == 0 <-> n == 0.
 Proof.
-intro n; rewrite NZeq_mul_0; tauto.
+intro n; rewrite eq_mul_0; tauto.
 Qed.
 
-Theorem NZeq_mul_0_l : forall n m : NZ, n * m == 0 -> m ~= 0 -> n == 0.
+Theorem eq_mul_0_l : forall n m, n * m == 0 -> m ~= 0 -> n == 0.
 Proof.
-intros n m H1 H2. apply -> NZeq_mul_0 in H1. destruct H1 as [H1 | H1].
+intros n m H1 H2. apply -> eq_mul_0 in H1. destruct H1 as [H1 | H1].
 assumption. false_hyp H1 H2.
 Qed.
 
-Theorem NZeq_mul_0_r : forall n m : NZ, n * m == 0 -> n ~= 0 -> m == 0.
+Theorem eq_mul_0_r : forall n m, n * m == 0 -> n ~= 0 -> m == 0.
 Proof.
-intros n m H1 H2; apply -> NZeq_mul_0 in H1. destruct H1 as [H1 | H1].
+intros n m H1 H2; apply -> eq_mul_0 in H1. destruct H1 as [H1 | H1].
 false_hyp H1 H2. assumption.
 Qed.
 
-Theorem NZlt_0_mul : forall n m : NZ, 0 < n * m <-> (0 < n /\ 0 < m) \/ (m < 0 /\ n < 0).
+Theorem lt_0_mul : forall n m, 0 < n * m <-> (0 < n /\ 0 < m) \/ (m < 0 /\ n < 0).
 Proof.
 intros n m; split; [intro H | intros [[H1 H2] | [H1 H2]]].
-destruct (NZlt_trichotomy n 0) as [H1 | [H1 | H1]];
-[| rewrite H1 in H; rewrite NZmul_0_l in H; false_hyp H NZlt_irrefl |];
-(destruct (NZlt_trichotomy m 0) as [H2 | [H2 | H2]];
-[| rewrite H2 in H; rewrite NZmul_0_r in H; false_hyp H NZlt_irrefl |]);
+destruct (lt_trichotomy n 0) as [H1 | [H1 | H1]];
+[| rewrite H1 in H; rewrite mul_0_l in H; false_hyp H lt_irrefl |];
+(destruct (lt_trichotomy m 0) as [H2 | [H2 | H2]];
+[| rewrite H2 in H; rewrite mul_0_r in H; false_hyp H lt_irrefl |]);
 try (left; now split); try (right; now split).
-assert (H3 : n * m < 0) by now apply NZmul_neg_pos.
-exfalso; now apply (NZlt_asymm (n * m) 0).
-assert (H3 : n * m < 0) by now apply NZmul_pos_neg.
-exfalso; now apply (NZlt_asymm (n * m) 0).
-now apply NZmul_pos_pos. now apply NZmul_neg_neg.
+assert (H3 : n * m < 0) by now apply mul_neg_pos.
+exfalso; now apply (lt_asymm (n * m) 0).
+assert (H3 : n * m < 0) by now apply mul_pos_neg.
+exfalso; now apply (lt_asymm (n * m) 0).
+now apply mul_pos_pos. now apply mul_neg_neg.
 Qed.
 
-Theorem NZsquare_lt_mono_nonneg : forall n m : NZ, 0 <= n -> n < m -> n * n < m * m.
+Theorem square_lt_mono_nonneg : forall n m, 0 <= n -> n < m -> n * n < m * m.
 Proof.
-intros n m H1 H2. now apply NZmul_lt_mono_nonneg.
+intros n m H1 H2. now apply mul_lt_mono_nonneg.
 Qed.
 
-Theorem NZsquare_le_mono_nonneg : forall n m : NZ, 0 <= n -> n <= m -> n * n <= m * m.
+Theorem square_le_mono_nonneg : forall n m, 0 <= n -> n <= m -> n * n <= m * m.
 Proof.
-intros n m H1 H2. now apply NZmul_le_mono_nonneg.
+intros n m H1 H2. now apply mul_le_mono_nonneg.
 Qed.
 
 (* The converse theorems require nonnegativity (or nonpositivity) of the
 other variable *)
 
-Theorem NZsquare_lt_simpl_nonneg : forall n m : NZ, 0 <= m -> n * n < m * m -> n < m.
+Theorem square_lt_simpl_nonneg : forall n m, 0 <= m -> n * n < m * m -> n < m.
 Proof.
-intros n m H1 H2. destruct (NZlt_ge_cases n 0).
-now apply NZlt_le_trans with 0.
-destruct (NZlt_ge_cases n m).
-assumption. assert (F : m * m <= n * n) by now apply NZsquare_le_mono_nonneg.
-apply -> NZle_ngt in F. false_hyp H2 F.
+intros n m H1 H2. destruct (lt_ge_cases n 0).
+now apply lt_le_trans with 0.
+destruct (lt_ge_cases n m).
+assumption. assert (F : m * m <= n * n) by now apply square_le_mono_nonneg.
+apply -> le_ngt in F. false_hyp H2 F.
 Qed.
 
-Theorem NZsquare_le_simpl_nonneg : forall n m : NZ, 0 <= m -> n * n <= m * m -> n <= m.
+Theorem square_le_simpl_nonneg : forall n m, 0 <= m -> n * n <= m * m -> n <= m.
 Proof.
-intros n m H1 H2. destruct (NZlt_ge_cases n 0).
-apply NZlt_le_incl; now apply NZlt_le_trans with 0.
-destruct (NZle_gt_cases n m).
-assumption. assert (F : m * m < n * n) by now apply NZsquare_lt_mono_nonneg.
-apply -> NZlt_nge in F. false_hyp H2 F.
+intros n m H1 H2. destruct (lt_ge_cases n 0).
+apply lt_le_incl; now apply lt_le_trans with 0.
+destruct (le_gt_cases n m).
+assumption. assert (F : m * m < n * n) by now apply square_lt_mono_nonneg.
+apply -> lt_nge in F. false_hyp H2 F.
 Qed.
 
-Theorem NZmul_2_mono_l : forall n m : NZ, n < m -> 1 + (1 + 1) * n < (1 + 1) * m.
+Theorem mul_2_mono_l : forall n m, n < m -> 1 + (1 + 1) * n < (1 + 1) * m.
 Proof.
-intros n m H. apply <- NZle_succ_l in H.
-apply -> (NZmul_le_mono_pos_l (S n) m (1 + 1)) in H.
-repeat rewrite NZmul_add_distr_r in *; repeat rewrite NZmul_1_l in *.
-repeat rewrite NZadd_succ_r in *. repeat rewrite NZadd_succ_l in *. rewrite NZadd_0_l.
-now apply -> NZle_succ_l.
-apply NZadd_pos_pos; now apply NZlt_succ_diag_r.
+intros n m. rewrite <- le_succ_l, (mul_le_mono_pos_l (S n) m (1 + 1)).
+rewrite !mul_add_distr_r; nzsimpl; now rewrite le_succ_l.
+apply add_pos_pos; now apply lt_0_1.
 Qed.
 
 End NZMulOrderPropFunct.
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 85b284a727..4c54cc3b86 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -13,648 +13,663 @@
 Require Import NZAxioms.
 Require Import NZMul.
 Require Import Decidable.
+Require Import OrderTac.
 
-Module NZOrderPropFunct (Import NZOrdAxiomsMod : NZOrdAxiomsSig).
-Module Export NZMulPropMod := NZMulPropFunct NZAxiomsMod.
-Open Local Scope NatIntScope.
+Module NZOrderPropFunct (Import NZ : NZOrdAxiomsSig).
+Include NZMulPropFunct NZ. (* In fact only NZBase is used here *)
+Local Open Scope NumScope.
 
-Ltac le_elim H := rewrite NZlt_eq_cases in H; destruct H as [H | H].
-
-Theorem NZlt_le_incl : forall n m : NZ, n < m -> n <= m.
+Instance le_wd : Proper (eq==>eq==>iff) le.
 Proof.
-intros; apply <- NZlt_eq_cases; now left.
+intros n n' Hn m m' Hm. rewrite !lt_eq_cases, !Hn, !Hm; auto with *.
 Qed.
 
-Theorem NZeq_le_incl : forall n m : NZ, n == m -> n <= m.
-Proof.
-intros; apply <- NZlt_eq_cases; now right.
-Qed.
+Ltac le_elim H := rewrite lt_eq_cases in H; destruct H as [H | H].
 
-Lemma NZlt_stepl : forall x y z : NZ, x < y -> x == z -> z < y.
+Theorem lt_le_incl : forall n m, n < m -> n <= m.
 Proof.
-intros x y z H1 H2; now rewrite <- H2.
+intros; apply <- lt_eq_cases; now left.
 Qed.
 
-Lemma NZlt_stepr : forall x y z : NZ, x < y -> y == z -> x < z.
+Theorem le_refl : forall n, n <= n.
 Proof.
-intros x y z H1 H2; now rewrite <- H2.
+intro; apply <- lt_eq_cases; now right.
 Qed.
 
-Lemma NZle_stepl : forall x y z : NZ, x <= y -> x == z -> z <= y.
+Theorem lt_succ_diag_r : forall n, n < S n.
 Proof.
-intros x y z H1 H2; now rewrite <- H2.
+intro n. rewrite lt_succ_r. apply le_refl.
 Qed.
 
-Lemma NZle_stepr : forall x y z : NZ, x <= y -> y == z -> x <= z.
+Theorem le_succ_diag_r : forall n, n <= S n.
 Proof.
-intros x y z H1 H2; now rewrite <- H2.
+intro; apply lt_le_incl; apply lt_succ_diag_r.
 Qed.
 
-Declare Left  Step NZlt_stepl.
-Declare Right Step NZlt_stepr.
-Declare Left  Step NZle_stepl.
-Declare Right Step NZle_stepr.
-
-Theorem NZlt_neq : forall n m : NZ, n < m -> n ~= m.
+Theorem neq_succ_diag_l : forall n, S n ~= n.
 Proof.
-intros n m H1 H2; rewrite H2 in H1; false_hyp H1 NZlt_irrefl.
+intros n H. apply (lt_irrefl n). rewrite <- H at 2. apply lt_succ_diag_r.
 Qed.
 
-Theorem NZle_neq : forall n m : NZ, n < m <-> n <= m /\ n ~= m.
+Theorem neq_succ_diag_r : forall n, n ~= S n.
 Proof.
-intros n m; split; [intro H | intros [H1 H2]].
-split. now apply NZlt_le_incl. now apply NZlt_neq.
-le_elim H1. assumption. false_hyp H1 H2.
+intro n; apply neq_sym, neq_succ_diag_l.
 Qed.
 
-Theorem NZle_refl : forall n : NZ, n <= n.
+Theorem nlt_succ_diag_l : forall n, ~ S n < n.
 Proof.
-intro; now apply NZeq_le_incl.
+intros n H. apply (lt_irrefl (S n)). rewrite lt_succ_r. now apply lt_le_incl.
 Qed.
 
-Theorem NZlt_succ_diag_r : forall n : NZ, n < S n.
+Theorem nle_succ_diag_l : forall n, ~ S n <= n.
 Proof.
-intro n. rewrite NZlt_succ_r. now apply NZeq_le_incl.
+intros n H; le_elim H.
+false_hyp H nlt_succ_diag_l. false_hyp H neq_succ_diag_l.
 Qed.
 
-Theorem NZle_succ_diag_r : forall n : NZ, n <= S n.
+Theorem le_succ_l : forall n m, S n <= m <-> n < m.
 Proof.
-intro; apply NZlt_le_incl; apply NZlt_succ_diag_r.
+intro n; nzinduct m n.
+split; intro H. false_hyp H nle_succ_diag_l. false_hyp H lt_irrefl.
+intro m.
+rewrite (lt_eq_cases (S n) (S m)), !lt_succ_r, (lt_eq_cases n m), succ_inj_wd.
+rewrite or_cancel_r.
+reflexivity.
+intros LE EQ; rewrite EQ in LE; false_hyp LE nle_succ_diag_l.
+intros LT EQ; rewrite EQ in LT; false_hyp LT lt_irrefl.
 Qed.
 
-Theorem NZlt_0_1 : 0 < 1.
-Proof.
-apply NZlt_succ_diag_r.
-Qed.
+(** Trichotomy *)
 
-Theorem NZle_0_1 : 0 <= 1.
+Theorem le_gt_cases : forall n m, n <= m \/ n > m.
 Proof.
-apply NZle_succ_diag_r.
+intros n m; nzinduct n m.
+left; apply le_refl.
+intro n. rewrite lt_succ_r, le_succ_l, !lt_eq_cases. intuition.
 Qed.
 
-Theorem NZlt_lt_succ_r : forall n m : NZ, n < m -> n < S m.
+Theorem lt_trichotomy : forall n m,  n < m \/ n == m \/ m < n.
 Proof.
-intros. rewrite NZlt_succ_r. now apply NZlt_le_incl.
+intros n m. generalize (le_gt_cases n m); rewrite lt_eq_cases; tauto.
 Qed.
 
-Theorem NZle_le_succ_r : forall n m : NZ, n <= m -> n <= S m.
-Proof.
-intros n m H. rewrite <- NZlt_succ_r in H. now apply NZlt_le_incl.
-Qed.
+Notation lt_eq_gt_cases := lt_trichotomy (only parsing).
+
+(** Asymmetry and transitivity. *)
 
-Theorem NZle_succ_r : forall n m : NZ, n <= S m <-> n <= m \/ n == S m.
+Theorem lt_asymm : forall n m, n < m -> ~ m < n.
 Proof.
-intros n m; rewrite NZlt_eq_cases. now rewrite NZlt_succ_r.
+intros n m; nzinduct n m.
+intros H; false_hyp H lt_irrefl.
+intro n; split; intros H H1 H2.
+apply lt_succ_r in H2. le_elim H2.
+apply H; auto. apply -> le_succ_l. now apply lt_le_incl.
+rewrite H2 in H1. false_hyp H1 nlt_succ_diag_l.
+apply le_succ_l in H1. le_elim H1.
+apply H; auto. rewrite lt_succ_r. now apply lt_le_incl.
+rewrite <- H1 in H2. false_hyp H2 nlt_succ_diag_l.
 Qed.
 
-(* The following theorem is a special case of neq_succ_iter_l below,
-but we prove it separately *)
+Notation lt_ngt := lt_asymm (only parsing).
 
-Theorem NZneq_succ_diag_l : forall n : NZ, S n ~= n.
+Theorem lt_trans : forall n m p, n < m -> m < p -> n < p.
 Proof.
-intros n H. pose proof (NZlt_succ_diag_r n) as H1. rewrite H in H1.
-false_hyp H1 NZlt_irrefl.
+intros n m p; nzinduct p m.
+intros _ H; false_hyp H lt_irrefl.
+intro p. rewrite 2 lt_succ_r.
+split; intros H H1 H2.
+apply lt_le_incl; le_elim H2; [now apply H | now rewrite H2 in H1].
+assert (n <= p) as H3 by (auto using lt_le_incl).
+le_elim H3. assumption. rewrite <- H3 in H2.
+elim (lt_asymm n m); auto.
 Qed.
 
-Theorem NZneq_succ_diag_r : forall n : NZ, n ~= S n.
-Proof.
-intro n; apply NZneq_sym; apply NZneq_succ_diag_l.
-Qed.
+(** We know enough now to benefit from the generic [order] tactic. *)
 
-Theorem NZnlt_succ_diag_l : forall n : NZ, ~ S n < n.
-Proof.
-intros n H; apply NZlt_lt_succ_r in H. false_hyp H NZlt_irrefl.
-Qed.
+Module OrderElts.
+ Definition t := t.
+ Definition eq := eq.
+ Definition lt := lt.
+ Definition le := le.
+ Instance eq_equiv : Equivalence eq.
+ Instance lt_strorder : StrictOrder lt.
+ Proof. split; [ exact lt_irrefl | exact lt_trans ]. Qed.
+ Instance lt_compat : Proper (eq==>eq==>iff) lt.
+ Proof. exact lt_wd. Qed. (* BUG(?) pourquoi ne trouve-t'il pas lt_wd *)
+ Definition lt_total := lt_trichotomy.
+ Definition le_lteq := lt_eq_cases.
+End OrderElts.
+Module OrderTac := MakeOrderTac OrderElts.
+Ltac order :=
+  change eq with OrderElts.eq in *;
+  change lt with OrderElts.lt in *;
+  change le with OrderElts.le in *;
+  OrderTac.order.
 
-Theorem NZnle_succ_diag_l : forall n : NZ, ~ S n <= n.
-Proof.
-intros n H; le_elim H.
-false_hyp H NZnlt_succ_diag_l. false_hyp H NZneq_succ_diag_l.
-Qed.
+(** Some direct consequences of [order]. *)
+
+Theorem lt_neq : forall n m, n < m -> n ~= m.
+Proof. order. Qed.
+
+Theorem le_neq : forall n m, n < m <-> n <= m /\ n ~= m.
+Proof. intuition order. Qed.
+
+Theorem eq_le_incl : forall n m, n == m -> n <= m.
+Proof. order. Qed.
+
+Lemma lt_stepl : forall x y z, x < y -> x == z -> z < y.
+Proof. order. Qed.
+
+Lemma lt_stepr : forall x y z, x < y -> y == z -> x < z.
+Proof. order. Qed.
+
+Lemma le_stepl : forall x y z, x <= y -> x == z -> z <= y.
+Proof. order. Qed.
+
+Lemma le_stepr : forall x y z, x <= y -> y == z -> x <= z.
+Proof. order. Qed.
+
+Declare Left  Step lt_stepl.
+Declare Right Step lt_stepr.
+Declare Left  Step le_stepl.
+Declare Right Step le_stepr.
 
-Theorem NZle_succ_l : forall n m : NZ, S n <= m <-> n < m.
+Theorem le_trans : forall n m p, n <= m -> m <= p -> n <= p.
+Proof. order. Qed.
+
+Theorem le_lt_trans : forall n m p, n <= m -> m < p -> n < p.
+Proof. order. Qed.
+
+Theorem lt_le_trans : forall n m p, n < m -> m <= p -> n < p.
+Proof. order. Qed.
+
+Theorem le_antisymm : forall n m, n <= m -> m <= n -> n == m.
+Proof. order. Qed.
+
+(** More properties of [<] and [<=] with respect to [S] and [0]. *)
+
+Theorem le_succ_r : forall n m, n <= S m <-> n <= m \/ n == S m.
 Proof.
-intro n; NZinduct m n.
-setoid_replace (n < n) with False using relation iff by
-  (apply -> neg_false; apply NZlt_irrefl).
-now setoid_replace (S n <= n) with False using relation iff by
-  (apply -> neg_false; apply NZnle_succ_diag_l).
-intro m. rewrite NZlt_succ_r. rewrite NZle_succ_r.
-rewrite NZsucc_inj_wd.
-rewrite (NZlt_eq_cases n m).
-rewrite or_cancel_r.
-reflexivity.
-intros H1 H2; rewrite H2 in H1; false_hyp H1 NZnle_succ_diag_l.
-apply NZlt_neq.
+intros n m; rewrite lt_eq_cases. now rewrite lt_succ_r.
 Qed.
 
-Theorem NZlt_succ_l : forall n m : NZ, S n < m -> n < m.
+Theorem lt_succ_l : forall n m, S n < m -> n < m.
 Proof.
-intros n m H; apply -> NZle_succ_l; now apply NZlt_le_incl.
+intros n m H; apply -> le_succ_l; now apply lt_le_incl.
 Qed.
 
-Theorem NZsucc_lt_mono : forall n m : NZ, n < m <-> S n < S m.
+Theorem le_le_succ_r : forall n m, n <= m -> n <= S m.
 Proof.
-intros n m. rewrite <- NZle_succ_l. symmetry. apply NZlt_succ_r.
+intros n m LE. rewrite <- lt_succ_r in LE. now apply lt_le_incl.
 Qed.
 
-Theorem NZsucc_le_mono : forall n m : NZ, n <= m <-> S n <= S m.
+Theorem lt_lt_succ_r : forall n m, n < m -> n < S m.
 Proof.
-intros n m. do 2 rewrite NZlt_eq_cases.
-rewrite <- NZsucc_lt_mono; now rewrite NZsucc_inj_wd.
+intros. rewrite lt_succ_r. now apply lt_le_incl.
 Qed.
 
-Theorem NZlt_asymm : forall n m, n < m -> ~ m < n.
+Theorem succ_lt_mono : forall n m, n < m <-> S n < S m.
 Proof.
-intros n m; NZinduct n m.
-intros H _; false_hyp H NZlt_irrefl.
-intro n; split; intros H H1 H2.
-apply NZlt_succ_l in H1. apply -> NZlt_succ_r in H2. le_elim H2.
-now apply H. rewrite H2 in H1; false_hyp H1 NZlt_irrefl.
-apply NZlt_lt_succ_r in H2. apply <- NZle_succ_l in H1. le_elim H1.
-now apply H. rewrite H1 in H2; false_hyp H2 NZlt_irrefl.
+intros n m. rewrite <- le_succ_l. symmetry. apply lt_succ_r.
 Qed.
 
-Theorem NZlt_trans : forall n m p : NZ, n < m -> m < p -> n < p.
+Theorem succ_le_mono : forall n m, n <= m <-> S n <= S m.
 Proof.
-intros n m p; NZinduct p m.
-intros _ H; false_hyp H NZlt_irrefl.
-intro p. do 2 rewrite NZlt_succ_r.
-split; intros H H1 H2.
-apply NZlt_le_incl; le_elim H2; [now apply H | now rewrite H2 in H1].
-assert (n <= p) as H3. apply H. assumption. now apply NZlt_le_incl.
-le_elim H3. assumption. rewrite <- H3 in H2.
-exfalso; now apply (NZlt_asymm n m).
+intros n m. now rewrite 2 lt_eq_cases, <- succ_lt_mono, succ_inj_wd.
 Qed.
 
-Theorem NZle_trans : forall n m p : NZ, n <= m -> m <= p -> n <= p.
+Theorem lt_0_1 : 0 < 1.
 Proof.
-intros n m p H1 H2; le_elim H1.
-le_elim H2. apply NZlt_le_incl; now apply NZlt_trans with (m := m).
-apply NZlt_le_incl; now rewrite <- H2. now rewrite H1.
+apply lt_succ_diag_r.
 Qed.
 
-Theorem NZle_lt_trans : forall n m p : NZ, n <= m -> m < p -> n < p.
+Theorem le_0_1 : 0 <= 1.
 Proof.
-intros n m p H1 H2; le_elim H1.
-now apply NZlt_trans with (m := m). now rewrite H1.
+apply le_succ_diag_r.
 Qed.
 
-Theorem NZlt_le_trans : forall n m p : NZ, n < m -> m <= p -> n < p.
+Theorem lt_1_l : forall n m, 0 < n -> n < m -> 1 < m.
 Proof.
-intros n m p H1 H2; le_elim H2.
-now apply NZlt_trans with (m := m). now rewrite <- H2.
+intros n m H1 H2. apply <- le_succ_l in H1. now apply le_lt_trans with n.
 Qed.
 
-Theorem NZle_antisymm : forall n m : NZ, n <= m -> m <= n -> n == m.
+
+(** More Trichotomy, decidability and double negation elimination. *)
+
+(** The following theorem is cleary redundant, but helps not to
+remember whether one has to say le_gt_cases or lt_ge_cases *)
+
+Theorem lt_ge_cases : forall n m, n < m \/ n >= m.
 Proof.
-intros n m H1 H2; now (le_elim H1; le_elim H2);
-[exfalso; apply (NZlt_asymm n m) | | |].
+intros n m; destruct (le_gt_cases m n); [right|left]; order.
 Qed.
 
-Theorem NZlt_1_l : forall n m : NZ, 0 < n -> n < m -> 1 < m.
+Theorem le_ge_cases : forall n m, n <= m \/ n >= m.
 Proof.
-intros n m H1 H2. apply <- NZle_succ_l in H1. now apply NZle_lt_trans with n.
+intros n m; destruct (le_gt_cases n m); [left|right]; order.
 Qed.
 
-(** Trichotomy, decidability, and double negation elimination *)
-
-Theorem NZlt_trichotomy : forall n m : NZ,  n < m \/ n == m \/ m < n.
+Theorem lt_gt_cases : forall n m, n ~= m <-> n < m \/ n > m.
 Proof.
-intros n m; NZinduct n m.
-right; now left.
-intro n; rewrite NZlt_succ_r. stepr ((S n < m \/ S n == m) \/ m <= n) by tauto.
-rewrite <- (NZlt_eq_cases (S n) m).
-setoid_replace (n == m) with (m == n) using relation iff by now split.
-stepl (n < m \/ m < n \/ m == n) by tauto. rewrite <- NZlt_eq_cases.
-apply or_iff_compat_r. symmetry; apply NZle_succ_l.
+intros n m; destruct (lt_trichotomy n m); intuition order.
 Qed.
 
-(* Decidability of equality, even though true in each finite ring, does not
+(** Decidability of equality, even though true in each finite ring, does not
 have a uniform proof. Otherwise, the proof for two fixed numbers would
 reduce to a normal form that will say if the numbers are equal or not,
 which cannot be true in all finite rings. Therefore, we prove decidability
 in the presence of order. *)
 
-Theorem NZeq_dec : forall n m : NZ, decidable (n == m).
+Theorem eq_dec : forall n m, decidable (n == m).
 Proof.
-intros n m; destruct (NZlt_trichotomy n m) as [H | [H | H]].
-right; intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl.
-now left.
-right; intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl.
+intros n m; destruct (lt_trichotomy n m) as [ | [ | ]];
+ (right; order) || (left; order).
 Qed.
 
-(* DNE stands for double-negation elimination *)
+(** DNE stands for double-negation elimination *)
 
-Theorem NZeq_dne : forall n m, ~ ~ n == m <-> n == m.
+Theorem eq_dne : forall n m, ~ ~ n == m <-> n == m.
 Proof.
 intros n m; split; intro H.
-destruct (NZeq_dec n m) as [H1 | H1].
+destruct (eq_dec n m) as [H1 | H1].
 assumption. false_hyp H1 H.
 intro H1; now apply H1.
 Qed.
 
-Theorem NZlt_gt_cases : forall n m : NZ, n ~= m <-> n < m \/ n > m.
-Proof.
-intros n m; split.
-pose proof (NZlt_trichotomy n m); tauto.
-intros H H1; destruct H as [H | H]; rewrite H1 in H; false_hyp H NZlt_irrefl.
-Qed.
-
-Theorem NZle_gt_cases : forall n m : NZ, n <= m \/ n > m.
-Proof.
-intros n m; destruct (NZlt_trichotomy n m) as [H | [H | H]].
-left; now apply NZlt_le_incl. left; now apply NZeq_le_incl. now right.
-Qed.
-
-(* The following theorem is cleary redundant, but helps not to
-remember whether one has to say le_gt_cases or lt_ge_cases *)
-
-Theorem NZlt_ge_cases : forall n m : NZ, n < m \/ n >= m.
-Proof.
-intros n m; destruct (NZle_gt_cases m n); try (now left); try (now right).
-Qed.
-
-Theorem NZle_ge_cases : forall n m : NZ, n <= m \/ n >= m.
-Proof.
-intros n m; destruct (NZle_gt_cases n m) as [H | H].
-now left. right; now apply NZlt_le_incl.
-Qed.
-
-Theorem NZle_ngt : forall n m : NZ, n <= m <-> ~ n > m.
-Proof.
-intros n m. split; intro H; [intro H1 |].
-eapply NZle_lt_trans in H; [| eassumption ..]. false_hyp H NZlt_irrefl.
-destruct (NZle_gt_cases n m) as [H1 | H1].
-assumption. false_hyp H1 H.
-Qed.
+Theorem le_ngt : forall n m, n <= m <-> ~ n > m.
+Proof. intuition order. Qed.
 
-(* Redundant but useful *)
+(** Redundant but useful *)
 
-Theorem NZnlt_ge : forall n m : NZ, ~ n < m <-> n >= m.
-Proof.
-intros n m; symmetry; apply NZle_ngt.
-Qed.
+Theorem nlt_ge : forall n m, ~ n < m <-> n >= m.
+Proof. intuition order. Qed.
 
-Theorem NZlt_dec : forall n m : NZ, decidable (n < m).
+Theorem lt_dec : forall n m, decidable (n < m).
 Proof.
-intros n m; destruct (NZle_gt_cases m n);
-[right; now apply -> NZle_ngt | now left].
+intros n m; destruct (le_gt_cases m n); [right|left]; order.
 Qed.
 
-Theorem NZlt_dne : forall n m, ~ ~ n < m <-> n < m.
+Theorem lt_dne : forall n m, ~ ~ n < m <-> n < m.
 Proof.
-intros n m; split; intro H;
-[destruct (NZlt_dec n m) as [H1 | H1]; [assumption | false_hyp H1 H] |
-intro H1; false_hyp H H1].
+intros n m; split; intro H.
+destruct (lt_dec n m) as [H1 | H1]; [assumption | false_hyp H1 H].
+intro H1; false_hyp H H1.
 Qed.
 
-Theorem NZnle_gt : forall n m : NZ, ~ n <= m <-> n > m.
-Proof.
-intros n m. rewrite NZle_ngt. apply NZlt_dne.
-Qed.
+Theorem nle_gt : forall n m, ~ n <= m <-> n > m.
+Proof. intuition order. Qed.
 
-(* Redundant but useful *)
+(** Redundant but useful *)
 
-Theorem NZlt_nge : forall n m : NZ, n < m <-> ~ n >= m.
-Proof.
-intros n m; symmetry; apply NZnle_gt.
-Qed.
+Theorem lt_nge : forall n m, n < m <-> ~ n >= m.
+Proof. intuition order. Qed.
 
-Theorem NZle_dec : forall n m : NZ, decidable (n <= m).
+Theorem le_dec : forall n m, decidable (n <= m).
 Proof.
-intros n m; destruct (NZle_gt_cases n m);
-[now left | right; now apply <- NZnle_gt].
+intros n m; destruct (le_gt_cases n m); [left|right]; order.
 Qed.
 
-Theorem NZle_dne : forall n m : NZ, ~ ~ n <= m <-> n <= m.
+Theorem le_dne : forall n m, ~ ~ n <= m <-> n <= m.
 Proof.
-intros n m; split; intro H;
-[destruct (NZle_dec n m) as [H1 | H1]; [assumption | false_hyp H1 H] |
-intro H1; false_hyp H H1].
+intros n m; split; intro H.
+destruct (le_dec n m) as [H1 | H1]; [assumption | false_hyp H1 H].
+intro H1; false_hyp H H1.
 Qed.
 
-Theorem NZnlt_succ_r : forall n m : NZ, ~ m < S n <-> n < m.
+Theorem nlt_succ_r : forall n m, ~ m < S n <-> n < m.
 Proof.
-intros n m; rewrite NZlt_succ_r; apply NZnle_gt.
+intros n m; rewrite lt_succ_r; apply nle_gt.
 Qed.
 
-(* The difference between integers and natural numbers is that for
+(** The difference between integers and natural numbers is that for
 every integer there is a predecessor, which is not true for natural
 numbers. However, for both classes, every number that is bigger than
 some other number has a predecessor. The proof of this fact by regular
 induction does not go through, so we need to use strong
 (course-of-value) induction. *)
 
-Lemma NZlt_exists_pred_strong :
-  forall z n m : NZ, z < m -> m <= n -> exists k : NZ, m == S k /\ z <= k.
+Lemma lt_exists_pred_strong :
+  forall z n m, z < m -> m <= n -> exists k, m == S k /\ z <= k.
 Proof.
-intro z; NZinduct n z.
-intros m H1 H2; apply <- NZnle_gt in H1; false_hyp H2 H1.
+intro z; nzinduct n z.
+order.
 intro n; split; intros IH m H1 H2.
-apply -> NZle_succ_r in H2; destruct H2 as [H2 | H2].
-now apply IH. exists n. now split; [| rewrite <- NZlt_succ_r; rewrite <- H2].
-apply IH. assumption. now apply NZle_le_succ_r.
+apply -> le_succ_r in H2. destruct H2 as [H2 | H2].
+now apply IH. exists n. now split; [| rewrite <- lt_succ_r; rewrite <- H2].
+apply IH. assumption. now apply le_le_succ_r.
 Qed.
 
-Theorem NZlt_exists_pred :
-  forall z n : NZ, z < n -> exists k : NZ, n == S k /\ z <= k.
+Theorem lt_exists_pred :
+  forall z n, z < n -> exists k, n == S k /\ z <= k.
 Proof.
-intros z n H; apply NZlt_exists_pred_strong with (z := z) (n := n).
-assumption. apply NZle_refl.
+intros z n H; apply lt_exists_pred_strong with (z := z) (n := n).
+assumption. apply le_refl.
 Qed.
 
 (** A corollary of having an order is that NZ is infinite *)
 
-(* This section about infinity of NZ relies on the type nat and can be
+(** This section about infinity of NZ relies on the type nat and can be
 safely removed *)
 
-Definition NZsucc_iter (n : nat) (m : NZ) :=
-  nat_rect (fun _ => NZ) m (fun _ l => S l) n.
+Fixpoint of_nat (n : nat) : t :=
+ match n with
+  | O => 0
+  | Datatypes.S n' => S (of_nat n')
+ end.
 
-Theorem NZlt_succ_iter_r :
-  forall (n : nat) (m : NZ), m < NZsucc_iter (Datatypes.S n) m.
+Theorem of_nat_S_gt_0 :
+  forall (n : nat), 0 < of_nat (Datatypes.S n).
 Proof.
-intros n m; induction n as [| n IH]; simpl in *.
-apply NZlt_succ_diag_r. now apply NZlt_lt_succ_r.
+intros n; induction n as [| n IH]; simpl in *.
+apply lt_0_1.
+apply lt_trans with 1. apply lt_0_1. now rewrite <- succ_lt_mono.
 Qed.
 
-Theorem NZneq_succ_iter_l :
-  forall (n : nat) (m : NZ), NZsucc_iter (Datatypes.S n) m ~= m.
+Theorem of_nat_S_neq_0 :
+  forall (n : nat), 0 ~= of_nat (Datatypes.S n).
 Proof.
-intros n m H. pose proof (NZlt_succ_iter_r n m) as H1. rewrite H in H1.
-false_hyp H1 NZlt_irrefl.
+intros. apply lt_neq, of_nat_S_gt_0.
 Qed.
 
-(* End of the section about the infinity of NZ *)
+Lemma of_nat_injective : forall n m, of_nat n == of_nat m -> n = m.
+Proof.
+induction n as [|n IH]; destruct m; auto.
+intros H; elim (of_nat_S_neq_0 _ H).
+intros H; symmetry in H; elim (of_nat_S_neq_0 _ H).
+intros. f_equal. apply IH. now rewrite <- succ_inj_wd.
+(* BUG: succ_inj_wd n'est pas vu par SearchAbout *)
+Qed.
+
+(** End of the section about the infinity of NZ *)
 
 (** Stronger variant of induction with assumptions n >= 0 (n < 0)
 in the induction step *)
 
 Section Induction.
 
-Variable A : NZ -> Prop.
-Hypothesis A_wd : Proper (NZeq==>iff) A.
+Variable A : t -> Prop.
+Hypothesis A_wd : Proper (eq==>iff) A.
 
 Section Center.
 
-Variable z : NZ. (* A z is the basis of induction *)
+Variable z : t. (* A z is the basis of induction *)
 
 Section RightInduction.
 
-Let A' (n : NZ) := forall m : NZ, z <= m -> m < n -> A m.
-Let right_step :=   forall n : NZ, z <= n -> A n -> A (S n).
-Let right_step' :=  forall n : NZ, z <= n -> A' n -> A n.
-Let right_step'' := forall n : NZ, A' n <-> A' (S n).
+Let A' (n : t) := forall m, z <= m -> m < n -> A m.
+Let right_step :=   forall n, z <= n -> A n -> A (S n).
+Let right_step' :=  forall n, z <= n -> A' n -> A n.
+Let right_step'' := forall n, A' n <-> A' (S n).
 
-Lemma NZrs_rs' :  A z -> right_step -> right_step'.
+Lemma rs_rs' :  A z -> right_step -> right_step'.
 Proof.
 intros Az RS n H1 H2.
-le_elim H1. apply NZlt_exists_pred in H1. destruct H1 as [k [H3 H4]].
-rewrite H3. apply RS; [assumption | apply H2; [assumption | rewrite H3; apply NZlt_succ_diag_r]].
+le_elim H1. apply lt_exists_pred in H1. destruct H1 as [k [H3 H4]].
+rewrite H3. apply RS; trivial. apply H2; trivial.
+rewrite H3; apply lt_succ_diag_r.
 rewrite <- H1; apply Az.
 Qed.
 
-Lemma NZrs'_rs'' : right_step' -> right_step''.
+Lemma rs'_rs'' : right_step' -> right_step''.
 Proof.
 intros RS' n; split; intros H1 m H2 H3.
-apply -> NZlt_succ_r in H3; le_elim H3;
+apply -> lt_succ_r in H3; le_elim H3;
 [now apply H1 | rewrite H3 in *; now apply RS'].
-apply H1; [assumption | now apply NZlt_lt_succ_r].
+apply H1; [assumption | now apply lt_lt_succ_r].
 Qed.
 
-Lemma NZrbase : A' z.
+Lemma rbase : A' z.
 Proof.
-intros m H1 H2. apply -> NZle_ngt in H1. false_hyp H2 H1.
+intros m H1 H2. apply -> le_ngt in H1. false_hyp H2 H1.
 Qed.
 
-Lemma NZA'A_right : (forall n : NZ, A' n) -> forall n : NZ, z <= n -> A n.
+Lemma A'A_right : (forall n, A' n) -> forall n, z <= n -> A n.
 Proof.
-intros H1 n H2. apply H1 with (n := S n); [assumption | apply NZlt_succ_diag_r].
+intros H1 n H2. apply H1 with (n := S n); [assumption | apply lt_succ_diag_r].
 Qed.
 
-Theorem NZstrong_right_induction: right_step' -> forall n : NZ, z <= n -> A n.
+Theorem strong_right_induction: right_step' -> forall n, z <= n -> A n.
 Proof.
-intro RS'; apply NZA'A_right; unfold A'; NZinduct n z;
-[apply NZrbase | apply NZrs'_rs''; apply RS'].
+intro RS'; apply A'A_right; unfold A'; nzinduct n z;
+[apply rbase | apply rs'_rs''; apply RS'].
 Qed.
 
-Theorem NZright_induction : A z -> right_step -> forall n : NZ, z <= n -> A n.
+Theorem right_induction : A z -> right_step -> forall n, z <= n -> A n.
 Proof.
-intros Az RS; apply NZstrong_right_induction; now apply NZrs_rs'.
+intros Az RS; apply strong_right_induction; now apply rs_rs'.
 Qed.
 
-Theorem NZright_induction' :
-  (forall n : NZ, n <= z -> A n) -> right_step -> forall n : NZ, A n.
+Theorem right_induction' :
+  (forall n, n <= z -> A n) -> right_step -> forall n, A n.
 Proof.
 intros L R n.
-destruct (NZlt_trichotomy n z) as [H | [H | H]].
-apply L; now apply NZlt_le_incl.
-apply L; now apply NZeq_le_incl.
-apply NZright_induction. apply L; now apply NZeq_le_incl. assumption. now apply NZlt_le_incl.
+destruct (lt_trichotomy n z) as [H | [H | H]].
+apply L; now apply lt_le_incl.
+apply L; now apply eq_le_incl.
+apply right_induction. apply L; now apply eq_le_incl. assumption.
+now apply lt_le_incl.
 Qed.
 
-Theorem NZstrong_right_induction' :
-  (forall n : NZ, n <= z -> A n) -> right_step' -> forall n : NZ, A n.
+Theorem strong_right_induction' :
+  (forall n, n <= z -> A n) -> right_step' -> forall n, A n.
 Proof.
 intros L R n.
-destruct (NZlt_trichotomy n z) as [H | [H | H]].
-apply L; now apply NZlt_le_incl.
-apply L; now apply NZeq_le_incl.
-apply NZstrong_right_induction. assumption. now apply NZlt_le_incl.
+destruct (lt_trichotomy n z) as [H | [H | H]].
+apply L; now apply lt_le_incl.
+apply L; now apply eq_le_incl.
+apply strong_right_induction. assumption. now apply lt_le_incl.
 Qed.
 
 End RightInduction.
 
 Section LeftInduction.
 
-Let A' (n : NZ) := forall m : NZ, m <= z -> n <= m -> A m.
-Let left_step :=   forall n : NZ, n < z -> A (S n) -> A n.
-Let left_step' :=  forall n : NZ, n <= z -> A' (S n) -> A n.
-Let left_step'' := forall n : NZ, A' n <-> A' (S n).
+Let A' (n : t) := forall m, m <= z -> n <= m -> A m.
+Let left_step :=   forall n, n < z -> A (S n) -> A n.
+Let left_step' :=  forall n, n <= z -> A' (S n) -> A n.
+Let left_step'' := forall n, A' n <-> A' (S n).
 
-Lemma NZls_ls' :  A z -> left_step -> left_step'.
+Lemma ls_ls' :  A z -> left_step -> left_step'.
 Proof.
 intros Az LS n H1 H2. le_elim H1.
-apply LS; [assumption | apply H2; [now apply <- NZle_succ_l | now apply NZeq_le_incl]].
+apply LS; trivial. apply H2; [now apply <- le_succ_l | now apply eq_le_incl].
 rewrite H1; apply Az.
 Qed.
 
-Lemma NZls'_ls'' : left_step' -> left_step''.
+Lemma ls'_ls'' : left_step' -> left_step''.
 Proof.
 intros LS' n; split; intros H1 m H2 H3.
-apply -> NZle_succ_l in H3. apply NZlt_le_incl in H3. now apply H1.
+apply -> le_succ_l in H3. apply lt_le_incl in H3. now apply H1.
 le_elim H3.
-apply <- NZle_succ_l in H3. now apply H1.
+apply <- le_succ_l in H3. now apply H1.
 rewrite <- H3 in *; now apply LS'.
 Qed.
 
-Lemma NZlbase : A' (S z).
+Lemma lbase : A' (S z).
 Proof.
-intros m H1 H2. apply -> NZle_succ_l in H2.
-apply -> NZle_ngt in H1. false_hyp H2 H1.
+intros m H1 H2. apply -> le_succ_l in H2.
+apply -> le_ngt in H1. false_hyp H2 H1.
 Qed.
 
-Lemma NZA'A_left : (forall n : NZ, A' n) -> forall n : NZ, n <= z -> A n.
+Lemma A'A_left : (forall n, A' n) -> forall n, n <= z -> A n.
 Proof.
-intros H1 n H2. apply H1 with (n := n); [assumption | now apply NZeq_le_incl].
+intros H1 n H2. apply H1 with (n := n); [assumption | now apply eq_le_incl].
 Qed.
 
-Theorem NZstrong_left_induction: left_step' -> forall n : NZ, n <= z -> A n.
+Theorem strong_left_induction: left_step' -> forall n, n <= z -> A n.
 Proof.
-intro LS'; apply NZA'A_left; unfold A'; NZinduct n (S z);
-[apply NZlbase | apply NZls'_ls''; apply LS'].
+intro LS'; apply A'A_left; unfold A'; nzinduct n (S z);
+[apply lbase | apply ls'_ls''; apply LS'].
 Qed.
 
-Theorem NZleft_induction : A z -> left_step -> forall n : NZ, n <= z -> A n.
+Theorem left_induction : A z -> left_step -> forall n, n <= z -> A n.
 Proof.
-intros Az LS; apply NZstrong_left_induction; now apply NZls_ls'.
+intros Az LS; apply strong_left_induction; now apply ls_ls'.
 Qed.
 
-Theorem NZleft_induction' :
-  (forall n : NZ, z <= n -> A n) -> left_step -> forall n : NZ, A n.
+Theorem left_induction' :
+  (forall n, z <= n -> A n) -> left_step -> forall n, A n.
 Proof.
 intros R L n.
-destruct (NZlt_trichotomy n z) as [H | [H | H]].
-apply NZleft_induction. apply R. now apply NZeq_le_incl. assumption. now apply NZlt_le_incl.
-rewrite H; apply R; now apply NZeq_le_incl.
-apply R; now apply NZlt_le_incl.
+destruct (lt_trichotomy n z) as [H | [H | H]].
+apply left_induction. apply R. now apply eq_le_incl. assumption.
+now apply lt_le_incl.
+rewrite H; apply R; now apply eq_le_incl.
+apply R; now apply lt_le_incl.
 Qed.
 
-Theorem NZstrong_left_induction' :
-  (forall n : NZ, z <= n -> A n) -> left_step' -> forall n : NZ, A n.
+Theorem strong_left_induction' :
+  (forall n, z <= n -> A n) -> left_step' -> forall n, A n.
 Proof.
 intros R L n.
-destruct (NZlt_trichotomy n z) as [H | [H | H]].
-apply NZstrong_left_induction; auto. now apply NZlt_le_incl.
-rewrite H; apply R; now apply NZeq_le_incl.
-apply R; now apply NZlt_le_incl.
+destruct (lt_trichotomy n z) as [H | [H | H]].
+apply strong_left_induction; auto. now apply lt_le_incl.
+rewrite H; apply R; now apply eq_le_incl.
+apply R; now apply lt_le_incl.
 Qed.
 
 End LeftInduction.
 
-Theorem NZorder_induction :
+Theorem order_induction :
   A z ->
-  (forall n : NZ, z <= n -> A n -> A (S n)) ->
-  (forall n : NZ, n < z  -> A (S n) -> A n) ->
-    forall n : NZ, A n.
+  (forall n, z <= n -> A n -> A (S n)) ->
+  (forall n, n < z  -> A (S n) -> A n) ->
+    forall n, A n.
 Proof.
 intros Az RS LS n.
-destruct (NZlt_trichotomy n z) as [H | [H | H]].
-now apply NZleft_induction; [| | apply NZlt_le_incl].
+destruct (lt_trichotomy n z) as [H | [H | H]].
+now apply left_induction; [| | apply lt_le_incl].
 now rewrite H.
-now apply NZright_induction; [| | apply NZlt_le_incl].
+now apply right_induction; [| | apply lt_le_incl].
 Qed.
 
-Theorem NZorder_induction' :
+Theorem order_induction' :
   A z ->
-  (forall n : NZ, z <= n -> A n -> A (S n)) ->
-  (forall n : NZ, n <= z -> A n -> A (P n)) ->
-    forall n : NZ, A n.
+  (forall n, z <= n -> A n -> A (S n)) ->
+  (forall n, n <= z -> A n -> A (P n)) ->
+    forall n, A n.
 Proof.
-intros Az AS AP n; apply NZorder_induction; try assumption.
-intros m H1 H2. apply AP in H2; [| now apply <- NZle_succ_l].
-apply -> (A_wd (P (S m)) m); [assumption | apply NZpred_succ].
+intros Az AS AP n; apply order_induction; try assumption.
+intros m H1 H2. apply AP in H2; [| now apply <- le_succ_l].
+apply -> (A_wd (P (S m)) m); [assumption | apply pred_succ].
 Qed.
 
 End Center.
 
-Theorem NZorder_induction_0 :
+Theorem order_induction_0 :
   A 0 ->
-  (forall n : NZ, 0 <= n -> A n -> A (S n)) ->
-  (forall n : NZ, n < 0  -> A (S n) -> A n) ->
-    forall n : NZ, A n.
-Proof (NZorder_induction 0).
+  (forall n, 0 <= n -> A n -> A (S n)) ->
+  (forall n, n < 0  -> A (S n) -> A n) ->
+    forall n, A n.
+Proof (order_induction 0).
 
-Theorem NZorder_induction'_0 :
+Theorem order_induction'_0 :
   A 0 ->
-  (forall n : NZ, 0 <= n -> A n -> A (S n)) ->
-  (forall n : NZ, n <= 0 -> A n -> A (P n)) ->
-    forall n : NZ, A n.
-Proof (NZorder_induction' 0).
+  (forall n, 0 <= n -> A n -> A (S n)) ->
+  (forall n, n <= 0 -> A n -> A (P n)) ->
+    forall n, A n.
+Proof (order_induction' 0).
 
 (** Elimintation principle for < *)
 
-Theorem NZlt_ind : forall (n : NZ),
+Theorem lt_ind : forall (n : t),
   A (S n) ->
-  (forall m : NZ, n < m -> A m -> A (S m)) ->
-   forall m : NZ, n < m -> A m.
+  (forall m, n < m -> A m -> A (S m)) ->
+   forall m, n < m -> A m.
 Proof.
 intros n H1 H2 m H3.
-apply NZright_induction with (S n); [assumption | | now apply <- NZle_succ_l].
-intros; apply H2; try assumption. now apply -> NZle_succ_l.
+apply right_induction with (S n); [assumption | | now apply <- le_succ_l].
+intros; apply H2; try assumption. now apply -> le_succ_l.
 Qed.
 
 (** Elimintation principle for <= *)
 
-Theorem NZle_ind : forall (n : NZ),
+Theorem le_ind : forall (n : t),
   A n ->
-  (forall m : NZ, n <= m -> A m -> A (S m)) ->
-   forall m : NZ, n <= m -> A m.
+  (forall m, n <= m -> A m -> A (S m)) ->
+   forall m, n <= m -> A m.
 Proof.
 intros n H1 H2 m H3.
-now apply NZright_induction with n.
+now apply right_induction with n.
 Qed.
 
 End Induction.
 
-Tactic Notation "NZord_induct" ident(n) :=
-  induction_maker n ltac:(apply NZorder_induction_0).
+Tactic Notation "nzord_induct" ident(n) :=
+  induction_maker n ltac:(apply order_induction_0).
 
-Tactic Notation "NZord_induct" ident(n) constr(z) :=
-  induction_maker n ltac:(apply NZorder_induction with z).
+Tactic Notation "nzord_induct" ident(n) constr(z) :=
+  induction_maker n ltac:(apply order_induction with z).
 
 Section WF.
 
-Variable z : NZ.
+Variable z : t.
 
-Let Rlt (n m : NZ) := z <= n /\ n < m.
-Let Rgt (n m : NZ) := m < n /\ n <= z.
+Let Rlt (n m : t) := z <= n /\ n < m.
+Let Rgt (n m : t) := m < n /\ n <= z.
 
-Instance Rlt_wd : Proper (NZeq ==> NZeq ==> iff) Rlt.
+Instance Rlt_wd : Proper (eq ==> eq ==> iff) Rlt.
 Proof.
 intros x1 x2 H1 x3 x4 H2; unfold Rlt. rewrite H1; now rewrite H2.
 Qed.
 
-Instance Rgt_wd : Proper (NZeq ==> NZeq ==> iff) Rgt.
+Instance Rgt_wd : Proper (eq ==> eq ==> iff) Rgt.
 Proof.
 intros x1 x2 H1 x3 x4 H2; unfold Rgt; rewrite H1; now rewrite H2.
 Qed.
 
-Instance NZAcc_lt_wd : Proper (NZeq==>iff) (Acc Rlt).
+Instance Acc_lt_wd : Proper (eq==>iff) (Acc Rlt).
 Proof.
 intros x1 x2 H; split; intro H1; destruct H1 as [H2];
 constructor; intros; apply H2; now (rewrite H || rewrite <- H).
 Qed.
 
-Instance NZAcc_gt_wd : Proper (NZeq==>iff) (Acc Rgt).
+Instance Acc_gt_wd : Proper (eq==>iff) (Acc Rgt).
 Proof.
 intros x1 x2 H; split; intro H1; destruct H1 as [H2];
 constructor; intros; apply H2; now (rewrite H || rewrite <- H).
 Qed.
 
-Theorem NZlt_wf : well_founded Rlt.
+Theorem lt_wf : well_founded Rlt.
 Proof.
 unfold well_founded.
-apply NZstrong_right_induction' with (z := z).
-apply NZAcc_lt_wd.
+apply strong_right_induction' with (z := z).
+apply Acc_lt_wd.
 intros n H; constructor; intros y [H1 H2].
-apply <- NZnle_gt in H2. elim H2. now apply NZle_trans with z.
+apply <- nle_gt in H2. elim H2. now apply le_trans with z.
 intros n H1 H2; constructor; intros m [H3 H4]. now apply H2.
 Qed.
 
-Theorem NZgt_wf : well_founded Rgt.
+Theorem gt_wf : well_founded Rgt.
 Proof.
 unfold well_founded.
-apply NZstrong_left_induction' with (z := z).
-apply NZAcc_gt_wd.
+apply strong_left_induction' with (z := z).
+apply Acc_gt_wd.
 intros n H; constructor; intros y [H1 H2].
-apply <- NZnle_gt in H2. elim H2. now apply NZle_lt_trans with n.
+apply <- nle_gt in H2. elim H2. now apply le_lt_trans with n.
 intros n H1 H2; constructor; intros m [H3 H4].
-apply H2. assumption. now apply <- NZle_succ_l.
+apply H2. assumption. now apply <- le_succ_l.
 Qed.
 
 End WF.
 
+(** * Compatibility of [min] and [max]. *)
+
+Instance min_wd : Proper (eq==>eq==>eq) min.
+Proof.
+intros n n' Hn m m' Hm.
+destruct (le_ge_cases n m).
+rewrite 2 min_l; auto. now rewrite <-Hn,<-Hm.
+rewrite 2 min_r; auto. now rewrite <-Hn,<-Hm.
+Qed.
+
+Instance max_wd : Proper (eq==>eq==>eq) max.
+Proof.
+intros n n' Hn m m' Hm.
+destruct (le_ge_cases n m).
+rewrite 2 max_r; auto. now rewrite <-Hn,<-Hm.
+rewrite 2 max_l; auto. now rewrite <-Hn,<-Hm.
+Qed.
+
 End NZOrderPropFunct.
 
diff --git a/theories/Numbers/NatInt/NZProperties.v b/theories/Numbers/NatInt/NZProperties.v
new file mode 100644
index 0000000000..781d065943
--- /dev/null
+++ b/theories/Numbers/NatInt/NZProperties.v
@@ -0,0 +1,20 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+Require Export NZAxioms NZMulOrder.
+
+(** This functor summarizes all known facts about NZ.
+    For the moment it is only an alias to [NZMulOrderPropFunct], which
+    subsumes all others.
+*)
+
+Module NZPropFunct := NZMulOrderPropFunct.