Update on Numbers; renamed ZOrder.v to ZLt to remove clash with ZArith/Zorder on MacOS.

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

7 files changed, 195 insertions, 233 deletions

diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index 7cfff8e030..86a828d037 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -64,5 +64,8 @@ Axiom recursion_succ :
     Aeq a a -> fun2_wd Neq Aeq Aeq f ->
       forall n : N, Aeq (recursion a f (S n)) (f n (recursion a f n)).
 
+(*Axiom dep_rec :
+  forall A : N -> Type, A 0 -> (forall n : N, A n -> A (S n)) -> forall n : N, A n.*)
+
 End NAxiomsSig.
 
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index d71f98057f..bcef668677 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -10,6 +10,7 @@
 
 (*i i*)
 
+Require Export Decidable.
 Require Export NAxioms.
 Require Import NZTimesOrder. (* The last property functor on NZ, which subsumes all others *)
 
@@ -59,8 +60,8 @@ Proof NZsucc_inj_wd_neg.
 (* Decidability and stability of equality was proved only in NZOrder, but
 since it does not mention order, we'll put it here *)
 
-Theorem eq_em : forall n m : N, n == m \/ n ~= m.
-Proof NZeq_em.
+Theorem eq_dec : forall n m : N, decidable (n == m).
+Proof NZeq_dec.
 
 Theorem eq_dne : forall n m : N, ~ ~ n == m <-> n == m.
 Proof NZeq_dne.
@@ -99,16 +100,21 @@ pattern false at 2; replace false with (if_zero false true 0) by apply if_zero_0
 now rewrite H.
 Qed.
 
+Theorem neq_0_succ : forall n : N, 0 ~= S n.
+Proof.
+intro n; apply neq_symm; apply neq_succ_0.
+Qed.
+
 (* Next, we show that all numbers are nonnegative and recover regular induction
 from the bidirectional induction on NZ *)
 
 Theorem le_0_l : forall n : N, 0 <= n.
 Proof.
 NZinduct n.
-le_equal.
+now apply NZeq_le_incl.
 intro n; split.
-apply NZle_le_succ.
-intro H; apply -> NZle_succ_le_or_eq_succ in H; destruct H as [H | H].
+apply NZle_le_succ_r.
+intro H; apply -> NZle_succ_r in H; destruct H as [H | H].
 assumption.
 symmetry in H; false_hyp H neq_succ_0.
 Qed.
@@ -144,7 +150,7 @@ Proof.
 intro H; apply (neq_succ_0 0). apply H.
 Qed.
 
-Theorem neq_0_succ : forall n, n ~= 0 <-> exists m, n == S m.
+Theorem neq_0_r : forall n, n ~= 0 <-> exists m, n == S m.
 Proof.
 cases n. split; intro H;
 [now elim H | destruct H as [m H]; symmetry in H; false_hyp H neq_succ_0].
diff --git a/theories/Numbers/Natural/Abstract/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v
index c109ff904a..f7c9cf19bb 100644
--- a/theories/Numbers/Natural/Abstract/NMinus.v
+++ b/theories/Numbers/Natural/Abstract/NMinus.v
@@ -63,8 +63,8 @@ Proof.
 intros n m p; induct p.
 intro; now do 2 rewrite minus_0_r.
 intros p IH H. do 2 rewrite minus_succ_r.
-rewrite <- IH; [now apply le_succ_le |].
-rewrite plus_pred_r. apply minus_gt. now apply <- lt_le_succ.
+rewrite <- IH; [apply lt_le_incl; now apply -> le_succ_l |].
+rewrite plus_pred_r. apply minus_gt. now apply -> le_succ_l.
 reflexivity.
 Qed.
 
@@ -129,7 +129,7 @@ Qed.
 Theorem le_minus_l : forall n m : N, n - m <= n.
 Proof.
 intro n; induct m.
-rewrite minus_0_r; le_equal.
+rewrite minus_0_r; now apply eq_le_incl.
 intros m IH. rewrite minus_succ_r.
 apply le_trans with (n - m); [apply le_pred_l | assumption].
 Qed.
@@ -150,7 +150,7 @@ Proof.
 intros n m; cases m.
 now rewrite pred_0, times_0_r, minus_0_l.
 intro m; rewrite pred_succ, times_succ_r, <- plus_minus_assoc.
-le_equal.
+now apply eq_le_incl.
 now rewrite minus_diag, plus_0_r.
 Qed.
 
@@ -163,7 +163,7 @@ rewrite minus_succ_l; [assumption |]. do 2 rewrite times_succ_l.
 rewrite (plus_comm ((n - m) * p) p), (plus_comm (n * p) p).
 rewrite <- (plus_minus_assoc p (n * p) (m * p)); [now apply times_le_mono_r |].
 now apply <- plus_cancel_l.
-assert (H1 : S n <= m); [now apply -> lt_le_succ |].
+assert (H1 : S n <= m); [now apply <- le_succ_l |].
 setoid_replace (S n - m) with 0 by now apply <- minus_0_le.
 setoid_replace ((S n * p) - m * p) with 0 by (apply <- minus_0_le; now apply times_le_mono_r).
 apply times_0_l.
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index bc3aace381..33214cd1bf 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -36,14 +36,14 @@ Theorem max_wd :
   forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> max n1 m1 == max n2 m2.
 Proof NZmax_wd.
 
-Theorem le_lt_or_eq : forall n m : N, n <= m <-> n < m \/ n == m.
-Proof NZle_lt_or_eq.
+Theorem lt_eq_cases : forall n m : N, n <= m <-> n < m \/ n == m.
+Proof NZlt_eq_cases.
 
 Theorem lt_irrefl : forall n : N, ~ n < n.
 Proof NZlt_irrefl.
 
-Theorem lt_succ_le : forall n m : N, n < S m <-> n <= m.
-Proof NZlt_succ_le.
+Theorem lt_succ_r : forall n m : N, n < S m <-> n <= m.
+Proof NZlt_succ_r.
 
 Theorem min_l : forall n m : N, n <= m -> min n m == n.
 Proof NZmin_l.
@@ -62,47 +62,50 @@ Proof NZmax_r.
 Theorem lt_le_incl : forall n m : N, n < m -> n <= m.
 Proof NZlt_le_incl.
 
+Theorem eq_le_incl : forall n m : N, n == m -> n <= m.
+Proof NZeq_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_neq : forall n m : N, n < m <-> n <= m /\ n ~= m.
+Proof NZle_neq.
 
 Theorem le_refl : forall n : N, n <= n.
 Proof NZle_refl.
 
-Theorem lt_succ_r : forall n : N, n < S n.
-Proof NZlt_succ_r.
+Theorem lt_succ_diag_r : forall n : N, n < S n.
+Proof NZlt_succ_diag_r.
 
-Theorem le_succ_r : forall n : N, n <= S n.
-Proof NZle_succ_r.
+Theorem le_succ_diag_r : forall n : N, n <= S n.
+Proof NZle_succ_diag_r.
 
-Theorem lt_lt_succ : forall n m : N, n < m -> n < S m.
-Proof NZlt_lt_succ.
+Theorem lt_lt_succ_r : forall n m : N, n < m -> n < S m.
+Proof NZlt_lt_succ_r.
 
-Theorem le_le_succ : forall n m : N, n <= m -> n <= S m.
-Proof NZle_le_succ.
+Theorem le_le_succ_r : forall n m : N, n <= m -> n <= S m.
+Proof NZle_le_succ_r.
 
-Theorem le_succ_le_or_eq_succ : forall n m : N, n <= S m <-> n <= m \/ n == S m.
-Proof NZle_succ_le_or_eq_succ.
+Theorem le_succ_r : forall n m : N, n <= S m <-> n <= m \/ n == S m.
+Proof NZle_succ_r.
 
-Theorem neq_succ_l : forall n : N, S n ~= n.
-Proof NZneq_succ_l.
+Theorem neq_succ_diag_l : forall n : N, S n ~= n.
+Proof NZneq_succ_diag_l.
 
-Theorem nlt_succ_l : forall n : N, ~ S n < n.
-Proof NZnlt_succ_l.
+Theorem neq_succ_diag_r : forall n : N, n ~= S n.
+Proof NZneq_succ_diag_r.
 
-Theorem nle_succ_l : forall n : N, ~ S n <= n.
-Proof NZnle_succ_l.
+Theorem nlt_succ_diag_l : forall n : N, ~ S n < n.
+Proof NZnlt_succ_diag_l.
 
-Theorem lt_le_succ : forall n m : N, n < m <-> S n <= m.
-Proof NZlt_le_succ.
+Theorem nle_succ_diag_l : forall n : N, ~ S n <= n.
+Proof NZnle_succ_diag_l.
 
-Theorem lt_succ_lt : forall n m : N, S n < m -> n < m.
-Proof NZlt_succ_lt.
+Theorem le_succ_l : forall n m : N, S n <= m <-> n < m.
+Proof NZle_succ_l.
 
-Theorem le_succ_le : forall n m : N, S n <= m -> n <= m.
-Proof NZle_succ_le.
+Theorem lt_succ_l : forall n m : N, S n < m -> n < m.
+Proof NZlt_succ_l.
 
 Theorem succ_lt_mono : forall n m : N, n < m <-> S n < S m.
 Proof NZsucc_lt_mono.
@@ -110,9 +113,11 @@ Proof NZsucc_lt_mono.
 Theorem succ_le_mono : forall n m : N, n <= m <-> S n <= S m.
 Proof NZsucc_le_mono.
 
-Theorem lt_asymm : forall n m, n < m -> ~ m < n.
+Theorem lt_asymm : forall n m : N, n < m -> ~ m < n.
 Proof NZlt_asymm.
 
+Notation lt_ngt := lt_asymm (only parsing).
+
 Theorem lt_trans : forall n m p : N, n < m -> m < p -> n < p.
 Proof NZlt_trans.
 
@@ -133,6 +138,8 @@ Proof NZle_antisymm.
 Theorem lt_trichotomy : forall n m : N,  n < m \/ n == m \/ m < n.
 Proof NZlt_trichotomy.
 
+Notation lt_eq_gt_cases := lt_trichotomy (only parsing).
+
 Theorem lt_gt_cases : forall n m : N, n ~= m <-> n < m \/ n > m.
 Proof NZlt_gt_cases.
 
@@ -151,10 +158,10 @@ Proof NZle_ngt.
 Theorem nlt_ge : forall n m : N, ~ n < m <-> n >= m.
 Proof NZnlt_ge.
 
-Theorem lt_em : forall n m : N, n < m \/ ~ n < m.
-Proof NZlt_em.
+Theorem lt_dec : forall n m : N, decidable (n < m).
+Proof NZlt_dec.
 
-Theorem lt_dne : forall n m, ~ ~ n < m <-> n < m.
+Theorem lt_dne : forall n m : N, ~ ~ n < m <-> n < m.
 Proof NZlt_dne.
 
 Theorem nle_gt : forall n m : N, ~ n <= m <-> n > m.
@@ -163,14 +170,14 @@ Proof NZnle_gt.
 Theorem lt_nge : forall n m : N, n < m <-> ~ n >= m.
 Proof NZlt_nge.
 
-Theorem le_em : forall n m : N, n <= m \/ ~ n <= m.
-Proof NZle_em.
+Theorem le_dec : forall n m : N, decidable (n <= m).
+Proof NZle_dec.
 
 Theorem le_dne : forall n m : N, ~ ~ n <= m <-> n <= m.
 Proof NZle_dne.
 
-Theorem lt_nlt_succ : forall n m : N, n < m <-> ~ m < S n.
-Proof NZlt_nlt_succ.
+Theorem nlt_succ_r : forall n m : N, ~ m < S n <-> n < m.
+Proof NZnlt_succ_r.
 
 Theorem lt_exists_pred :
   forall z n : N, z < n -> exists k : N, n == S k /\ z <= k.
@@ -212,9 +219,9 @@ Proof NZright_induction'.
 Theorem left_induction' :
   forall A : N -> Prop, predicate_wd Neq A ->
     forall z : N,
-    (forall n : NZ, z <= n -> A n) ->
+    (forall n : N, z <= n -> A n) ->
     (forall n : N, n < z -> A (S n) -> A n) ->
-      forall n : NZ, A n.
+      forall n : N, A n.
 Proof NZleft_induction'.
 
 Theorem strong_right_induction :
@@ -313,35 +320,75 @@ Proof.
 intro n; apply -> le_ngt. apply le_0_l.
 Qed.
 
-Theorem nle_succ_0 : forall n, ~ (S n <= 0).
+Theorem nle_succ_0 : forall n : N, ~ (S n <= 0).
 Proof.
-intros n H; apply <- lt_le_succ in H; false_hyp H nlt_0_r.
+intros n H; apply -> le_succ_l in H; false_hyp H nlt_0_r.
 Qed.
 
-Theorem le_0_eq_0 : forall n, n <= 0 <-> n == 0.
+Theorem le_0_r : forall n : N, n <= 0 <-> n == 0.
 Proof.
 intros n; split; intro H.
 le_elim H; [false_hyp H nlt_0_r | assumption].
-le_equal.
+now apply eq_le_incl.
 Qed.
 
-Theorem lt_0_succ : forall n, 0 < S n.
+Theorem lt_0_succ : forall n : N, 0 < S n.
 Proof.
-induct n; [apply lt_succ_r | intros n H; now apply lt_lt_succ].
+induct n; [apply lt_succ_diag_r | intros n H; now apply lt_lt_succ_r].
 Qed.
 
-Theorem lt_lt_0 : forall n m, n < m -> 0 < m.
+Theorem neq_0_lt_0 : forall n : N, n ~= 0 <-> 0 < n.
+Proof.
+cases n.
+split; intro H; [now elim H | intro; now apply lt_irrefl with 0].
+intro n; split; intro H; [apply lt_0_succ | apply neq_succ_0].
+Qed.
+
+Theorem eq_0_gt_0_cases : forall n : N, n == 0 \/ 0 < n.
+Proof.
+cases n.
+now left.
+intro; right; apply lt_0_succ.
+Qed.
+
+Theorem zero_one : forall n : N, n == 0 \/ n == 1 \/ 1 < n.
+Proof.
+induct n. now left.
+cases n. intros; right; now left.
+intros n IH. destruct IH as [H | [H | H]].
+false_hyp H neq_succ_0.
+right; right. rewrite H. apply lt_succ_diag_r.
+right; right. now apply lt_lt_succ_r.
+Qed.
+
+Theorem lt_1_r : forall n : N, n < 1 <-> n == 0.
+Proof.
+cases n.
+split; intro; [reflexivity | apply lt_succ_diag_r].
+intros n. rewrite <- succ_lt_mono.
+split; intro H; [false_hyp H nlt_0_r | false_hyp H neq_succ_0].
+Qed.
+
+Theorem le_1_r : forall n : N, n <= 1 <-> n == 0 \/ n == 1.
+Proof.
+cases n.
+split; intro; [now left | apply le_succ_diag_r].
+intro n. rewrite <- succ_le_mono, le_0_r, succ_inj_wd.
+split; [intro; now right | intros [H | H]; [false_hyp H neq_succ_0 | assumption]].
+Qed.
+
+Theorem lt_lt_0 : forall n m : N, n < m -> 0 < m.
 Proof.
 intros n m; induct n.
 trivial.
-intros n IH H. apply IH; now apply lt_succ_lt.
+intros n IH H. apply IH; now apply lt_succ_l.
 Qed.
 
-Theorem neq_0_lt_0 : forall n, n ~= 0 <-> 0 < n.
+Theorem lt_1_l : forall n m p : N, n < m -> m < p -> 1 < p.
 Proof.
-cases n.
-split; intro H; [now elim H | intro; now apply lt_irrefl with 0].
-intro n; split; intro H; [apply lt_0_succ | apply neq_succ_0].
+intros n m p H1 H2.
+apply le_lt_trans with m. apply <- le_succ_l. apply le_lt_trans with n.
+apply le_0_l. assumption. assumption.
 Qed.
 
 (** Elimination principlies for < and <= for relations *)
@@ -357,30 +404,30 @@ Add Morphism R with signature Neq ==> Neq ==> iff as R_morph2.
 Proof R_wd.
 
 Theorem le_ind_rel :
-   (forall m, R 0 m) ->
-   (forall n m, n <= m -> R n m -> R (S n) (S m)) ->
-     forall n m, n <= m -> R n m.
+   (forall m : N, R 0 m) ->
+   (forall n m : N, n <= m -> R n m -> R (S n) (S m)) ->
+     forall n m : N, n <= m -> R n m.
 Proof.
 intros Base Step; induct n.
 intros; apply Base.
 intros n IH m H. elim H using le_ind.
 solve_predicate_wd.
-apply Step; [| apply IH]; now le_equal.
-intros k H1 H2. apply le_succ_le in H1. auto.
+apply Step; [| apply IH]; now apply eq_le_incl.
+intros k H1 H2. apply -> le_succ_l in H1. apply lt_le_incl in H1. auto.
 Qed.
 
 Theorem lt_ind_rel :
-   (forall m, R 0 (S m)) ->
-   (forall n m, n < m -> R n m -> R (S n) (S m)) ->
-   forall n m, n < m -> R n m.
+   (forall m : N, R 0 (S m)) ->
+   (forall n m : N, n < m -> R n m -> R (S n) (S m)) ->
+   forall n m : N, n < m -> R n m.
 Proof.
 intros Base Step; induct n.
 intros m H. apply lt_exists_pred in H; destruct H as [m' [H _]].
 rewrite H; apply Base.
 intros n IH m H. elim H using lt_ind.
 solve_predicate_wd.
-apply Step; [| apply IH]; now apply lt_succ_r.
-intros k H1 H2. apply lt_succ_lt in H1. auto.
+apply Step; [| apply IH]; now apply lt_succ_diag_r.
+intros k H1 H2. apply lt_succ_l in H1. auto.
 Qed.
 
 End RelElim.
@@ -396,15 +443,15 @@ Qed.
 Theorem le_pred_l : forall n : N, P n <= n.
 Proof.
 cases n.
-rewrite pred_0; le_equal.
-intros; rewrite pred_succ;  apply le_succ_r.
+rewrite pred_0; now apply eq_le_incl.
+intros; rewrite pred_succ;  apply le_succ_diag_r.
 Qed.
 
 Theorem lt_pred_l : forall n : N, n ~= 0 -> P n < n.
 Proof.
 cases n.
 intro H; elimtype False; now apply H.
-intros; rewrite pred_succ;  apply lt_succ_r.
+intros; rewrite pred_succ;  apply lt_succ_diag_r.
 Qed.
 
 Theorem le_le_pred : forall n m : N, n <= m -> P n <= m.
@@ -421,14 +468,14 @@ Theorem lt_le_pred : forall n m : N, n < m -> n <= P m. (* Converse is false for
 Proof.
 intro n; cases m.
 intro H; false_hyp H nlt_0_r.
-intros m IH. rewrite pred_succ; now apply -> lt_succ_le.
+intros m IH. rewrite pred_succ; now apply -> lt_succ_r.
 Qed.
 
 Theorem lt_pred_le : forall n m : N, P n < m -> n <= m. (* Converse is false for n == m == 0 *)
 Proof.
 intros n m; cases n.
-rewrite pred_0; intro H; le_less.
-intros n IH. rewrite pred_succ in IH. now apply -> lt_le_succ.
+rewrite pred_0; intro H; now apply lt_le_incl.
+intros n IH. rewrite pred_succ in IH. now apply <- le_succ_l.
 Qed.
 
 Theorem lt_pred_lt : forall n m : N, n < P m -> n < m.
@@ -467,12 +514,12 @@ Qed.
 
 Theorem le_succ_le_pred : forall n m : N, S n <= m -> n <= P m. (* Converse is false for n == m == 0 *)
 Proof.
-intros n m H. apply lt_le_pred. now apply <- lt_le_succ.
+intros n m H. apply lt_le_pred. now apply -> le_succ_l.
 Qed.
 
 Theorem lt_pred_lt_succ : forall n m : N, P n < m -> n < S m. (* Converse is false for n == m == 0 *)
 Proof.
-intros n m H. apply <- lt_succ_le. now apply lt_pred_le.
+intros n m H. apply <- lt_succ_r. now apply lt_pred_le.
 Qed.
 
 Theorem le_pred_le_succ : forall n m : N, P n <= m <-> n <= S m.
diff --git a/theories/Numbers/Natural/Abstract/NPlus.v b/theories/Numbers/Natural/Abstract/NPlus.v
index a033d95a09..d1269cf03f 100644
--- a/theories/Numbers/Natural/Abstract/NPlus.v
+++ b/theories/Numbers/Natural/Abstract/NPlus.v
@@ -61,7 +61,7 @@ Proof NZplus_cancel_r.
 
 (** Theorems that are valid for natural numbers but cannot be proved for Z *)
 
-Theorem plus_eq_0 : forall n m : N, n + m == 0 <-> n == 0 /\ m == 0.
+Theorem eq_plus_0 : forall n m : N, n + m == 0 <-> n == 0 /\ m == 0.
 Proof.
 intros n m; induct n.
 (* The next command does not work with the axiom plus_0_l from NPlusSig *)
@@ -73,7 +73,7 @@ setoid_replace (S n == 0) with False using relation iff by
  (apply -> neg_false; apply neq_succ_0). tauto.
 Qed.
 
-Theorem plus_eq_succ :
+Theorem eq_plus_succ :
   forall n m : N, (exists p : N, n + m == S p) <->
                     (exists n' : N, n == S n') \/ (exists m' : N, m == S m').
 Proof.
@@ -88,16 +88,16 @@ left; now exists n.
 exists (n + m); now rewrite plus_succ_l.
 Qed.
 
-Theorem plus_eq_1 : forall n m : N,
+Theorem eq_plus_1 : forall n m : N,
   n + m == 1 -> n == 1 /\ m == 0 \/ n == 0 /\ m == 1.
 Proof.
 intros n m H.
 assert (H1 : exists p : N, n + m == S p) by now exists 0.
-apply -> plus_eq_succ in H1. destruct H1 as [[n' H1] | [m' H1]].
+apply -> eq_plus_succ in H1. destruct H1 as [[n' H1] | [m' H1]].
 left. rewrite H1 in H; rewrite plus_succ_l in H; apply succ_inj in H.
-apply -> plus_eq_0 in H. destruct H as [H2 H3]; rewrite H2 in H1; now split.
+apply -> eq_plus_0 in H. destruct H as [H2 H3]; rewrite H2 in H1; now split.
 right. rewrite H1 in H; rewrite plus_succ_r in H; apply succ_inj in H.
-apply -> plus_eq_0 in H. destruct H as [H2 H3]; rewrite H3 in H1; now split.
+apply -> eq_plus_0 in H. destruct H as [H2 H3]; rewrite H3 in H1; now split.
 Qed.
 
 Theorem succ_plus_discr : forall n m : N, m ~= S (n + m).
diff --git a/theories/Numbers/Natural/Abstract/NTimes.v b/theories/Numbers/Natural/Abstract/NTimes.v
index 6a22e476da..e15f02a1ef 100644
--- a/theories/Numbers/Natural/Abstract/NTimes.v
+++ b/theories/Numbers/Natural/Abstract/NTimes.v
@@ -20,20 +20,20 @@ Theorem times_wd :
   forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> n1 * m1 == n2 * m2.
 Proof NZtimes_wd.
 
-Theorem times_0_r : forall n, n * 0 == 0.
-Proof NZtimes_0_r.
-
-Theorem times_succ_r : forall n m, n * (S m) == n * m + n.
-Proof NZtimes_succ_r.
-
-(** Theorems that are valid for both natural numbers and integers *)
-
 Theorem times_0_l : forall n : N, 0 * n == 0.
 Proof NZtimes_0_l.
 
 Theorem times_succ_l : forall n m : N, (S n) * m == n * m + m.
 Proof NZtimes_succ_l.
 
+(** Theorems that are valid for both natural numbers and integers *)
+
+Theorem times_0_r : forall n, n * 0 == 0.
+Proof NZtimes_0_r.
+
+Theorem times_succ_r : forall n m, n * (S m) == n * m + n.
+Proof NZtimes_succ_r.
+
 Theorem times_comm : forall n m : N, n * m == m * n.
 Proof NZtimes_comm.
 
@@ -54,28 +54,6 @@ Proof NZtimes_1_r.
 
 (** Theorems that cannot be proved in NZTimes *)
 
-Theorem times_eq_0 : forall n m, n * m == 0 -> n == 0 \/ m == 0.
-Proof.
-induct n; induct m.
-intros; now left.
-intros; now left.
-intros; now right.
-intros m IH H1. rewrite times_succ_l in H1.
-rewrite plus_succ_r in H1. now apply neq_succ_0 in H1.
-Qed.
-
-Theorem times_eq_1 : forall n m : N, n * m == 1 -> n == 1 /\ m == 1.
-Proof.
-intros n m; induct n.
-intro H; rewrite times_0_l in H; symmetry in H; false_hyp H neq_succ_0.
-intros n IH H. rewrite times_succ_l in H. apply plus_eq_1 in H.
-destruct H as [[H1 H2] | [H1 H2]].
-apply IH in H1. destruct H1 as [_ H1]. rewrite H1 in H2; false_hyp H2 neq_succ_0.
-apply times_eq_0 in H1. destruct H1 as [H1 | H1].
-rewrite H1; now split.
-rewrite H2 in H1; false_hyp H1 neq_succ_0.
-Qed.
-
 (* In proving the correctness of the definition of multiplication on
 integers constructed from pairs of natural numbers, we'll need the
 following fact about natural numbers:
diff --git a/theories/Numbers/Natural/Abstract/NTimesOrder.v b/theories/Numbers/Natural/Abstract/NTimesOrder.v
index ec010ecee9..d6c0bfafa1 100644
--- a/theories/Numbers/Natural/Abstract/NTimesOrder.v
+++ b/theories/Numbers/Natural/Abstract/NTimesOrder.v
@@ -10,118 +10,56 @@
 
 (*i i*)
 
-Require Export NOrder.
+Require Export NPlusOrder.
 
 Module NTimesOrderPropFunct (Import NAxiomsMod : NAxiomsSig).
-Module Export NOrderPropMod := NOrderPropFunct NAxiomsMod.
+Module Export NPlusOrderPropMod := NPlusOrderPropFunct NAxiomsMod.
 Open Local Scope NatScope.
 
-Theorem plus_lt_mono_l : forall n m p : N, n < m <-> p + n < p + m.
-Proof NZplus_lt_mono_l.
-
-Theorem plus_lt_mono_r : forall n m p : N, n < m <-> n + p < m + p.
-Proof NZplus_lt_mono_r.
-
-Theorem plus_lt_mono : forall n m p q : N, n < m -> p < q -> n + p < m + q.
-Proof NZplus_lt_mono.
-
-Theorem plus_le_mono_l : forall n m p : N, n <= m <-> p + n <= p + m.
-Proof NZplus_le_mono_l.
-
-Theorem plus_le_mono_r : forall n m p : N, n <= m <-> n + p <= m + p.
-Proof NZplus_le_mono_r.
-
-Theorem plus_le_mono : forall n m p q : N, n <= m -> p <= q -> n + p <= m + q.
-Proof NZplus_le_mono.
-
-Theorem plus_lt_le_mono : forall n m p q : N, n < m -> p <= q -> n + p < m + q.
-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_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 times_lt_pred :
+  forall p q n m : N, S p == q -> (p * n < p * m <-> q * n + m < q * m + n).
+Proof NZtimes_lt_pred.
 
-Theorem plus_le_cases : forall n m p q : N, n + m <= p + q -> n <= p \/ m <= q.
-Proof NZplus_le_cases.
+Theorem times_lt_mono_pos_l : forall p n m : N, 0 < p -> (n < m <-> p * n < p * m).
+Proof NZtimes_lt_mono_pos_l.
 
-Theorem plus_pos_cases : forall n m : N, 0 < n + m -> 0 < n \/ 0 < m.
-Proof NZplus_pos_cases.
+Theorem times_lt_mono_pos_r : forall p n m : N, 0 < p -> (n < m <-> n * p < m * p).
+Proof NZtimes_lt_mono_pos_r.
 
-(** Theorems true for natural numbers *)
+Theorem times_cancel_l : forall n m p : N, p ~= 0 -> (p * n == p * m <-> n == m).
+Proof NZtimes_cancel_l.
 
-Theorem le_plus_r : forall n m : N, n <= n + m.
-Proof.
-intro n; induct m.
-rewrite plus_0_r; le_equal.
-intros m IH. rewrite plus_succ_r; now apply le_le_succ.
-Qed.
+Theorem times_cancel_r : forall n m p : N, p ~= 0 -> (n * p == m * p <-> n == m).
+Proof NZtimes_cancel_r.
 
-Theorem lt_lt_plus_r : forall n m p : N, n < m -> n < m + p.
-Proof.
-intros n m p H; rewrite <- (plus_0_r n).
-apply plus_lt_le_mono; [assumption | apply le_0_l].
-Qed.
+Theorem times_le_mono_pos_l : forall n m p : N, 0 < p -> (n <= m <-> p * n <= p * m).
+Proof NZtimes_le_mono_pos_l.
 
-Theorem lt_lt_plus_l : forall n m p : N, n < m -> n < p + m.
-Proof.
-intros n m p; rewrite plus_comm; apply lt_lt_plus_r.
-Qed.
+Theorem times_le_mono_pos_r : forall n m p : N, 0 < p -> (n <= m <-> n * p <= m * p).
+Proof NZtimes_le_mono_pos_r.
 
-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 times_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n * m.
+Proof NZtimes_pos_pos.
 
-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.
+Theorem lt_1_times_pos : forall n m : N, 1 < n -> 0 < m -> 1 < n * m.
+Proof NZlt_1_times_pos.
 
-(* The following property is used to prove the correctness of the
-definition of order on integers constructed from pairs of natural numbers *)
+Theorem eq_times_0 : forall n m : N, n * m == 0 <-> n == 0 \/ m == 0.
+Proof NZeq_times_0.
 
-Theorem plus_lt_repl_pair : forall n m n' m' u v : N,
-  n + u < m + v -> n + m' == n' + m -> n' + u < m' + v.
-Proof.
-intros n m n' m' u v H1 H2.
-symmetry in H2. assert (H3 : n' + m <= n + m') by now le_equal.
-pose proof (plus_lt_le_mono _ _ _ _ H1 H3) as H4.
-rewrite (plus_shuffle2 n u), (plus_shuffle1 m v), (plus_comm m n) in H4.
-do 2 rewrite <- plus_assoc in H4. do 2 apply <- plus_lt_mono_l in H4.
-now rewrite (plus_comm n' u), (plus_comm m' v).
-Qed.
+Theorem neq_times_0 : forall n m : N, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
+Proof NZneq_times_0.
 
-(** Multiplication and order *)
+Theorem eq_times_0_l : forall n m : N, n * m == 0 -> m ~= 0 -> n == 0.
+Proof NZeq_times_0_l.
 
-Theorem times_lt_pred :
-  forall p q n m : N, S p == q -> (p * n < p * m <-> q * n + m < q * m + n).
-Proof NZtimes_lt_pred.
+Theorem eq_times_0_r : forall n m : N, n * m == 0 -> n ~= 0 -> m == 0.
+Proof NZeq_times_0_r.
 
-Theorem times_lt_mono_pos_l : forall p n m : N, 0 < p -> (n < m <-> p * n < p * m).
-Proof NZtimes_lt_mono_pos_l.
+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_lt_mono_pos_r : forall p n m : N, 0 < p -> (n < m <-> n * p < m * p).
-Proof NZtimes_lt_mono_pos_r.
+(** Theorems that are either not valid on Z or have different proofs on N and Z *)
 
 Theorem times_le_mono_l : forall n m p : N, n <= m -> p * n <= p * m.
 Proof.
@@ -133,18 +71,6 @@ Proof.
 intros; apply NZtimes_le_mono_nonneg_r. apply le_0_l. assumption.
 Qed.
 
-Theorem times_cancel_l : forall n m p : N, p ~= 0 -> (p * n == p * m <-> n == m).
-Proof NZtimes_cancel_l.
-
-Theorem times_cancel_r : forall n m p : N, p ~= 0 -> (n * p == m * p <-> n == m).
-Proof NZtimes_cancel_r.
-
-Theorem times_le_mono_pos_l : forall n m p : N, 0 < p -> (n <= m <-> p * n <= p * m).
-Proof NZtimes_le_mono_pos_l.
-
-Theorem times_le_mono_pos_r : forall n m p : N, 0 < p -> (n <= m <-> n * p <= m * p).
-Proof NZtimes_le_mono_pos_r.
-
 Theorem times_lt_mono : forall n m p q : N, n < m -> p < q -> n * p < m * q.
 Proof.
 intros; apply NZtimes_lt_mono; try assumption; apply le_0_l.
@@ -155,18 +81,6 @@ Proof.
 intros; apply NZtimes_le_mono; try assumption; apply le_0_l.
 Qed.
 
-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.
-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]].
@@ -174,5 +88,19 @@ apply -> NZtimes_pos in H. destruct H as [[H1 H2] | [H1 H2]]. now split. false_h
 now apply NZtimes_pos_pos.
 Qed.
 
+Theorem eq_times_1 : forall n m : N, n * m == 1 <-> n == 1 /\ m == 1.
+Proof.
+intros n m.
+split; [| intros [H1 H2]; now rewrite H1, H2, times_1_l].
+intro H; destruct (NZlt_trichotomy n 1) as [H1 | [H1 | H1]].
+apply -> lt_1_r in H1. rewrite H1, times_0_l in H. false_hyp H neq_0_succ.
+rewrite H1, times_1_l in H; now split.
+destruct (eq_0_gt_0_cases m) as [H2 | H2].
+rewrite H2, times_0_r in H; false_hyp H neq_0_succ.
+apply -> (times_lt_mono_pos_r m) in H1; [| assumption]. rewrite times_1_l in H1.
+assert (H3 : 1 < n * m) by now apply (lt_1_l 0 m).
+rewrite H in H3; false_hyp H3 lt_irrefl.
+Qed.
+
 End NTimesOrderPropFunct.