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

4 files changed, 163 insertions, 130 deletions

diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index 9c9161e2b..f218ed6a6 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -60,8 +60,8 @@ Axiom NZplus_succ_l : forall n m : NZ, (S n) + m == S (n + m).
 Axiom NZminus_0_r : forall n : NZ, n - 0 == n.
 Axiom NZminus_succ_r : forall n m : NZ, n - (S m) == P (n - m).
 
-Axiom NZtimes_0_r : forall n : NZ, n * 0 == 0.
-Axiom NZtimes_succ_r : forall n m : NZ, n * (S m) == n * m + n.
+Axiom NZtimes_0_l : forall n : NZ, 0 * n == 0.
+Axiom NZtimes_succ_l : forall n m : NZ, S n * m == n * m + m.
 
 End NZAxiomsSig.
 
@@ -84,9 +84,9 @@ 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 NZle_lt_or_eq : forall n m : NZ, n <= m <-> n < m \/ n == m.
+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_le : forall n m : NZ, n < S m <-> n <= m.
+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.
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 4ded2b892..df2f224f4 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -12,14 +12,23 @@
 
 Require Import NZAxioms.
 Require Import NZTimes.
+Require Import Decidable.
 
 Module NZOrderPropFunct (Import NZOrdAxiomsMod : NZOrdAxiomsSig).
 Module Export NZTimesPropMod := NZTimesPropFunct NZAxiomsMod.
 Open Local Scope NatIntScope.
 
-Ltac le_less := rewrite NZle_lt_or_eq; left; try assumption.
-Ltac le_equal := rewrite NZle_lt_or_eq; right; try reflexivity; try assumption.
-Ltac le_elim H := rewrite NZle_lt_or_eq in H; destruct H as [H | H].
+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.
+Proof.
+intros; apply <- NZlt_eq_cases; now left.
+Qed.
+
+Theorem NZeq_le_incl : forall n m : NZ, n == m -> n <= m.
+Proof.
+intros; apply <- NZlt_eq_cases; now right.
+Qed.
 
 Lemma NZlt_stepl : forall x y z : NZ, x < y -> x == z -> z < y.
 Proof.
@@ -46,106 +55,101 @@ Declare Right Step NZlt_stepr.
 Declare Left  Step NZle_stepl.
 Declare Right Step NZle_stepr.
 
-Theorem NZlt_le_incl : forall n m : NZ, n < m -> n <= m.
-Proof.
-intros; now le_less.
-Qed.
-
 Theorem NZlt_neq : forall n m : NZ, n < m -> n ~= m.
 Proof.
 intros n m H1 H2; rewrite H2 in H1; false_hyp H1 NZlt_irrefl.
 Qed.
 
-Theorem NZlt_le_neq : forall n m : NZ, n < m <-> n <= m /\ n ~= m.
+Theorem NZle_neq : forall n m : NZ, n < m <-> n <= m /\ n ~= m.
 Proof.
 intros n m; split; [intro H | intros [H1 H2]].
-split. le_less. now apply NZlt_neq.
+split. now apply NZlt_le_incl. now apply NZlt_neq.
 le_elim H1. assumption. false_hyp H1 H2.
 Qed.
 
 Theorem NZle_refl : forall n : NZ, n <= n.
 Proof.
-intro; now le_equal.
+intro; now apply NZeq_le_incl.
 Qed.
 
-Theorem NZlt_succ_r : forall n : NZ, n < S n.
+Theorem NZlt_succ_diag_r : forall n : NZ, n < S n.
 Proof.
-intro n. rewrite NZlt_succ_le. now le_equal.
+intro n. rewrite NZlt_succ_r. now apply NZeq_le_incl.
 Qed.
 
-Theorem NZle_succ_r : forall n : NZ, n <= S n.
+Theorem NZle_succ_diag_r : forall n : NZ, n <= S n.
 Proof.
-intro; le_less; apply NZlt_succ_r.
+intro; apply NZlt_le_incl; apply NZlt_succ_diag_r.
 Qed.
 
-Theorem NZlt_lt_succ : forall n m : NZ, n < m -> n < S m.
+Theorem NZlt_lt_succ_r : forall n m : NZ, n < m -> n < S m.
 Proof.
-intros. rewrite NZlt_succ_le. now le_less.
+intros. rewrite NZlt_succ_r. now apply NZlt_le_incl.
 Qed.
 
-Theorem NZle_le_succ : forall n m : NZ, n <= m -> n <= S m.
+Theorem NZle_le_succ_r : forall n m : NZ, n <= m -> n <= S m.
 Proof.
-intros n m H; rewrite <- NZlt_succ_le in H; now le_less.
+intros n m H. rewrite <- NZlt_succ_r in H. now apply NZlt_le_incl.
 Qed.
 
-Theorem NZle_succ_le_or_eq_succ : forall n m : NZ, n <= S m <-> n <= m \/ n == S m.
+Theorem NZle_succ_r : forall n m : NZ, n <= S m <-> n <= m \/ n == S m.
 Proof.
-intros n m; rewrite NZle_lt_or_eq. now rewrite NZlt_succ_le.
+intros n m; rewrite NZlt_eq_cases. now rewrite NZlt_succ_r.
 Qed.
 
 (* The following theorem is a special case of neq_succ_iter_l below,
-but we prove it independently *)
+but we prove it separately *)
 
-Theorem NZneq_succ_l : forall n : NZ, S n ~= n.
+Theorem NZneq_succ_diag_l : forall n : NZ, S n ~= n.
 Proof.
-intros n H. pose proof (NZlt_succ_r n) as H1. rewrite H in H1.
+intros n H. pose proof (NZlt_succ_diag_r n) as H1. rewrite H in H1.
 false_hyp H1 NZlt_irrefl.
 Qed.
 
-Theorem NZnlt_succ_l : forall n : NZ, ~ S n < n.
+Theorem NZneq_succ_diag_r : forall n : NZ, n ~= S n.
 Proof.
-intros n H; apply NZlt_lt_succ in H. false_hyp H NZlt_irrefl.
+intro n; apply NZneq_symm; apply NZneq_succ_diag_l.
 Qed.
 
-Theorem NZnle_succ_l : forall n : NZ, ~ S n <= n.
+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.
+
+Theorem NZnle_succ_diag_l : forall n : NZ, ~ S n <= n.
 Proof.
 intros n H; le_elim H.
-false_hyp H NZnlt_succ_l. false_hyp H NZneq_succ_l.
+false_hyp H NZnlt_succ_diag_l. false_hyp H NZneq_succ_diag_l.
 Qed.
 
-Theorem NZlt_le_succ : forall n m : NZ, n < m <-> S n <= m.
+Theorem NZle_succ_l : forall n m : NZ, S n <= m <-> n < 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_l).
-intro m. rewrite NZlt_succ_le. rewrite NZle_succ_le_or_eq_succ.
-rewrite NZsucc_inj_wd. rewrite (NZle_lt_or_eq n m).
+  (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.
+intros H1 H2; rewrite H2 in H1; false_hyp H1 NZnle_succ_diag_l.
 apply NZlt_neq.
-intros H1 H2; rewrite H2 in H1; false_hyp H1 NZnle_succ_l.
 reflexivity.
 Qed.
 
-Theorem NZlt_succ_lt : forall n m : NZ, S n < m -> n < m.
-Proof.
-intros n m H; apply <- NZlt_le_succ; now le_less.
-Qed.
-
-Theorem NZle_succ_le : forall n m : NZ, S n <= m -> n <= m.
+Theorem NZlt_succ_l : forall n m : NZ, S n < m -> n < m.
 Proof.
-intros n m H; le_less; now apply <- NZlt_le_succ.
+intros n m H; apply -> NZle_succ_l; now apply NZlt_le_incl.
 Qed.
 
 Theorem NZsucc_lt_mono : forall n m : NZ, n < m <-> S n < S m.
 Proof.
-intros n m. rewrite NZlt_le_succ. symmetry. apply NZlt_succ_le.
+intros n m. rewrite <- NZle_succ_l. symmetry. apply NZlt_succ_r.
 Qed.
 
 Theorem NZsucc_le_mono : forall n m : NZ, n <= m <-> S n <= S m.
 Proof.
-intros n m. do 2 rewrite NZle_lt_or_eq.
+intros n m. do 2 rewrite NZlt_eq_cases.
 rewrite <- NZsucc_lt_mono; now rewrite NZsucc_inj_wd.
 Qed.
 
@@ -154,9 +158,9 @@ Proof.
 intros n m; NZinduct n m.
 intros H _; false_hyp H NZlt_irrefl.
 intro n; split; intros H H1 H2.
-apply NZlt_succ_lt in H1. apply -> NZlt_succ_le in H2. le_elim 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 in H2. apply -> NZlt_le_succ in H1. le_elim H1.
+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.
 Qed.
 
@@ -164,10 +168,10 @@ Theorem NZlt_trans : forall n m p : NZ, n < m -> m < p -> n < p.
 Proof.
 intros n m p; NZinduct p m.
 intros _ H; false_hyp H NZlt_irrefl.
-intro p. do 2 rewrite NZlt_succ_le.
+intro p. do 2 rewrite NZlt_succ_r.
 split; intros H H1 H2.
-le_less; le_elim H2; [now apply H | now rewrite H2 in H1].
-assert (n <= p) as H3. apply H. assumption. now le_less.
+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.
 elimtype False; now apply (NZlt_asymm n m).
 Qed.
@@ -175,8 +179,8 @@ Qed.
 Theorem NZle_trans : forall n m p : NZ, n <= m -> m <= p -> n <= p.
 Proof.
 intros n m p H1 H2; le_elim H1.
-le_elim H2. le_less; now apply NZlt_trans with (m := m).
-le_less; now rewrite <- H2. now rewrite 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.
 Qed.
 
 Theorem NZle_lt_trans : forall n m p : NZ, n <= m -> m < p -> n < p.
@@ -197,17 +201,22 @@ intros n m H1 H2; now (le_elim H1; le_elim H2);
 [elimtype False; apply (NZlt_asymm n m) | | |].
 Qed.
 
+Theorem NZlt_1_l : forall n m : NZ, 0 < n -> n < m -> 1 < m.
+Proof.
+intros n m H1 H2. apply <- NZle_succ_l in H1. now apply NZle_lt_trans with n.
+Qed.
+
 (** Trichotomy, decidability, and double negation elimination *)
 
 Theorem NZlt_trichotomy : forall n m : NZ,  n < m \/ n == m \/ m < n.
 Proof.
 intros n m; NZinduct n m.
 right; now left.
-intro n; rewrite NZlt_succ_le. stepr ((S n < m \/ S n == m) \/ m <= n) by tauto.
-rewrite <- (NZle_lt_or_eq (S n) m).
+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 <- NZle_lt_or_eq.
-apply or_iff_compat_r. apply NZlt_le_succ.
+stepl (n < m \/ m < n \/ m == n) by tauto. rewrite <- NZlt_eq_cases.
+apply or_iff_compat_r. symmetry; apply NZle_succ_l.
 Qed.
 
 (* Decidability of equality, even though true in each finite ring, does not
@@ -215,7 +224,8 @@ 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_em : forall n m : NZ, n == m \/ n ~= m.
+
+Theorem NZeq_dec : forall n m : NZ, 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.
@@ -226,7 +236,7 @@ Qed.
 Theorem NZeq_dne : forall n m, ~ ~ n == m <-> n == m.
 Proof.
 intros n m; split; intro H.
-destruct (NZeq_em n m) as [H1 | H1].
+destruct (NZeq_dec n m) as [H1 | H1].
 assumption. false_hyp H1 H.
 intro H1; now apply H1.
 Qed.
@@ -241,7 +251,7 @@ 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 le_less. left; now le_equal. now right.
+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
@@ -255,7 +265,7 @@ 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; le_less.
+now left. right; now apply NZlt_le_incl.
 Qed.
 
 Theorem NZle_ngt : forall n m : NZ, n <= m <-> ~ n > m.
@@ -267,12 +277,13 @@ assumption. false_hyp H1 H.
 Qed.
 
 (* Redundant but useful *)
+
 Theorem NZnlt_ge : forall n m : NZ, ~ n < m <-> n >= m.
 Proof.
 intros n m; symmetry; apply NZle_ngt.
 Qed.
 
-Theorem NZlt_em : forall n m : NZ, n < m \/ ~ n < m.
+Theorem NZlt_dec : forall n m : NZ, decidable (n < m).
 Proof.
 intros n m; destruct (NZle_gt_cases m n);
 [right; now apply -> NZle_ngt | now left].
@@ -281,7 +292,7 @@ Qed.
 Theorem NZlt_dne : forall n m, ~ ~ n < m <-> n < m.
 Proof.
 intros n m; split; intro H;
-[destruct (NZlt_em n m) as [H1 | H1]; [assumption | false_hyp H1 H] |
+[destruct (NZlt_dec n m) as [H1 | H1]; [assumption | false_hyp H1 H] |
 intro H1; false_hyp H H1].
 Qed.
 
@@ -291,12 +302,13 @@ intros n m. rewrite NZle_ngt. apply NZlt_dne.
 Qed.
 
 (* Redundant but useful *)
+
 Theorem NZlt_nge : forall n m : NZ, n < m <-> ~ n >= m.
 Proof.
 intros n m; symmetry; apply NZnle_gt.
 Qed.
 
-Theorem NZle_em : forall n m : NZ, n <= m \/ ~ n <= m.
+Theorem NZle_dec : forall n m : NZ, decidable (n <= m).
 Proof.
 intros n m; destruct (NZle_gt_cases n m);
 [now left | right; now apply <- NZnle_gt].
@@ -305,13 +317,13 @@ Qed.
 Theorem NZle_dne : forall n m : NZ, ~ ~ n <= m <-> n <= m.
 Proof.
 intros n m; split; intro H;
-[destruct (NZle_em n m) as [H1 | H1]; [assumption | false_hyp H1 H] |
+[destruct (NZle_dec n m) as [H1 | H1]; [assumption | false_hyp H1 H] |
 intro H1; false_hyp H H1].
 Qed.
 
-Theorem NZlt_nlt_succ : forall n m : NZ, n < m <-> ~ m < S n.
+Theorem NZnlt_succ_r : forall n m : NZ, ~ m < S n <-> n < m.
 Proof.
-intros n m; rewrite NZlt_succ_le; symmetry; apply NZnle_gt.
+intros n m; rewrite NZlt_succ_r; apply NZnle_gt.
 Qed.
 
 (* The difference between integers and natural numbers is that for
@@ -327,9 +339,9 @@ Proof.
 intro z; NZinduct n z.
 intros m H1 H2; apply <- NZnle_gt in H1; false_hyp H2 H1.
 intro n; split; intros IH m H1 H2.
-apply -> NZle_succ_le_or_eq_succ in H2; destruct H2 as [H2 | H2].
-now apply IH. exists n. now split; [| rewrite <- NZlt_succ_le; rewrite <- H2].
-apply IH. assumption. now apply NZle_le_succ.
+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.
 Qed.
 
 Theorem NZlt_exists_pred :
@@ -351,7 +363,7 @@ Theorem NZlt_succ_iter_r :
   forall (n : nat) (m : NZ), m < NZsucc_iter (Datatypes.S n) m.
 Proof.
 intros n m; induction n as [| n IH]; simpl in *.
-apply NZlt_succ_r. now apply NZlt_lt_succ.
+apply NZlt_succ_diag_r. now apply NZlt_lt_succ_r.
 Qed.
 
 Theorem NZneq_succ_iter_l :
@@ -389,16 +401,16 @@ Lemma NZrs_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_r]].
+rewrite H3. apply RS; [assumption | apply H2; [assumption | rewrite H3; apply NZlt_succ_diag_r]].
 rewrite <- H1; apply Az.
 Qed.
 
 Lemma NZrs'_rs'' : right_step' -> right_step''.
 Proof.
 intros RS' n; split; intros H1 m H2 H3.
-apply -> NZlt_succ_le in H3; le_elim H3;
+apply -> NZlt_succ_r in H3; le_elim H3;
 [now apply H1 | rewrite H3 in *; now apply RS'].
-apply H1; [assumption | now apply NZlt_lt_succ].
+apply H1; [assumption | now apply NZlt_lt_succ_r].
 Qed.
 
 Lemma NZrbase : A' z.
@@ -408,7 +420,7 @@ Qed.
 
 Lemma NZA'A_right : (forall n : NZ, A' n) -> forall n : NZ, z <= n -> A n.
 Proof.
-intros H1 n H2. apply H1 with (n := S n); [assumption | apply NZlt_succ_r].
+intros H1 n H2. apply H1 with (n := S n); [assumption | apply NZlt_succ_diag_r].
 Qed.
 
 Theorem NZstrong_right_induction: right_step' -> forall n : NZ, z <= n -> A n.
@@ -427,9 +439,9 @@ Theorem NZright_induction' :
 Proof.
 intros L R n.
 destruct (NZlt_trichotomy n z) as [H | [H | H]].
-apply L; now le_less.
-apply L; now le_equal.
-apply NZright_induction. apply L; now le_equal. assumption. now le_less.
+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.
 Qed.
 
 Theorem NZstrong_right_induction' :
@@ -437,9 +449,9 @@ Theorem NZstrong_right_induction' :
 Proof.
 intros L R n.
 destruct (NZlt_trichotomy n z) as [H | [H | H]].
-apply L; now le_less.
-apply L; now le_equal.
-apply NZstrong_right_induction. assumption. now le_less.
+apply L; now apply NZlt_le_incl.
+apply L; now apply NZeq_le_incl.
+apply NZstrong_right_induction. assumption. now apply NZlt_le_incl.
 Qed.
 
 End RightInduction.
@@ -454,28 +466,28 @@ Let left_step'' := forall n : NZ, A' n <-> A' (S n).
 Lemma NZls_ls' :  A z -> left_step -> left_step'.
 Proof.
 intros Az LS n H1 H2. le_elim H1.
-apply LS; [assumption | apply H2; [now apply -> NZlt_le_succ | now le_equal]].
+apply LS; [assumption | apply H2; [now apply <- NZle_succ_l | now apply NZeq_le_incl]].
 rewrite H1; apply Az.
 Qed.
 
 Lemma NZls'_ls'' : left_step' -> left_step''.
 Proof.
 intros LS' n; split; intros H1 m H2 H3.
-apply NZle_succ_le in H3. now apply H1.
+apply -> NZle_succ_l in H3. apply NZlt_le_incl in H3. now apply H1.
 le_elim H3.
-apply -> NZlt_le_succ in H3. now apply H1.
+apply <- NZle_succ_l in H3. now apply H1.
 rewrite <- H3 in *; now apply LS'.
 Qed.
 
 Lemma NZlbase : A' (S z).
 Proof.
-intros m H1 H2. apply <- NZlt_le_succ in H2.
+intros m H1 H2. apply -> NZle_succ_l in H2.
 apply -> NZle_ngt in H1. false_hyp H2 H1.
 Qed.
 
 Lemma NZA'A_left : (forall n : NZ, A' n) -> forall n : NZ, n <= z -> A n.
 Proof.
-intros H1 n H2. apply H1 with (n := n); [assumption | now le_equal].
+intros H1 n H2. apply H1 with (n := n); [assumption | now apply NZeq_le_incl].
 Qed.
 
 Theorem NZstrong_left_induction: left_step' -> forall n : NZ, n <= z -> A n.
@@ -494,9 +506,9 @@ Theorem NZleft_induction' :
 Proof.
 intros R L n.
 destruct (NZlt_trichotomy n z) as [H | [H | H]].
-apply NZleft_induction. apply R. now le_equal. assumption. now le_less.
-rewrite H; apply R; le_equal.
-apply R; le_less.
+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.
 Qed.
 
 Theorem NZstrong_left_induction' :
@@ -504,9 +516,9 @@ Theorem NZstrong_left_induction' :
 Proof.
 intros R L n.
 destruct (NZlt_trichotomy n z) as [H | [H | H]].
-apply NZstrong_left_induction; auto. le_less.
-rewrite H; apply R; le_equal.
-apply R; le_less.
+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.
 Qed.
 
 End LeftInduction.
@@ -519,9 +531,9 @@ Theorem NZorder_induction :
 Proof.
 intros Az RS LS n.
 destruct (NZlt_trichotomy n z) as [H | [H | H]].
-now apply NZleft_induction; [| | le_less].
+now apply NZleft_induction; [| | apply NZlt_le_incl].
 now rewrite H.
-now apply NZright_induction; [| | le_less].
+now apply NZright_induction; [| | apply NZlt_le_incl].
 Qed.
 
 Theorem NZorder_induction' :
@@ -531,7 +543,7 @@ Theorem NZorder_induction' :
     forall n : NZ, A n.
 Proof.
 intros Az AS AP n; apply NZorder_induction; try assumption.
-intros m H1 H2. apply AP in H2; [| now apply -> NZlt_le_succ].
+intros m H1 H2. apply AP in H2; [| now apply <- NZle_succ_l].
 unfold predicate_wd, fun_wd in A_wd; apply -> (A_wd (P (S m)) m);
 [assumption | apply NZpred_succ].
 Qed.
@@ -560,8 +572,8 @@ Theorem NZlt_ind : forall (n : NZ),
    forall m : NZ, n < m -> A m.
 Proof.
 intros n H1 H2 m H3.
-apply NZright_induction with (S n); [assumption | | now apply -> NZlt_le_succ].
-intros; apply H2; try assumption. now apply <- NZlt_le_succ.
+apply NZright_induction with (S n); [assumption | | now apply <- NZle_succ_l].
+intros; apply H2; try assumption. now apply -> NZle_succ_l.
 Qed.
 
 (** Elimintation principle for <= *)
@@ -632,7 +644,7 @@ apply NZAcc_gt_wd.
 intros n H; constructor; intros y [H1 H2].
 apply <- NZnle_gt in H2. elim H2. now apply NZle_lt_trans with n.
 intros n H1 H2; constructor; intros m [H3 H4].
-apply H2. assumption. now apply -> NZlt_le_succ.
+apply H2. assumption. now apply <- NZle_succ_l.
 Qed.
 
 End WF.
diff --git a/theories/Numbers/NatInt/NZTimes.v b/theories/Numbers/NatInt/NZTimes.v
index e0d1f6350..20bd3cdc6 100644
--- a/theories/Numbers/NatInt/NZTimes.v
+++ b/theories/Numbers/NatInt/NZTimes.v
@@ -17,20 +17,20 @@ Module NZTimesPropFunct (Import NZAxiomsMod : NZAxiomsSig).
 Module Export NZPlusPropMod := NZPlusPropFunct NZAxiomsMod.
 Open Local Scope NatIntScope.
 
-Theorem NZtimes_0_l : forall n : NZ, 0 * n == 0.
+Theorem NZtimes_0_r : forall n : NZ, n * 0 == 0.
 Proof.
 NZinduct n.
-now rewrite NZtimes_0_r.
-intro. rewrite NZtimes_succ_r. now rewrite NZplus_0_r.
+now rewrite NZtimes_0_l.
+intro. rewrite NZtimes_succ_l. now rewrite NZplus_0_r.
 Qed.
 
-Theorem NZtimes_succ_l : forall n m : NZ, (S n) * m == n * m + m.
+Theorem NZtimes_succ_r : forall n m : NZ, n * (S m) == n * m + n.
 Proof.
-intros n m; NZinduct m.
-do 2 rewrite NZtimes_0_r; now rewrite NZplus_0_l.
-intro m. do 2 rewrite NZtimes_succ_r. do 2 rewrite NZplus_succ_r.
-rewrite NZsucc_inj_wd. rewrite <- (NZplus_assoc (n * m) n m).
-rewrite (NZplus_comm n m). rewrite NZplus_assoc.
+intros n m; NZinduct n.
+do 2 rewrite NZtimes_0_l; now rewrite NZplus_0_l.
+intro n. do 2 rewrite NZtimes_succ_l. do 2 rewrite NZplus_succ_r.
+rewrite NZsucc_inj_wd. rewrite <- (NZplus_assoc (n * m) m n).
+rewrite (NZplus_comm m n). rewrite NZplus_assoc.
 now rewrite NZplus_cancel_r.
 Qed.
 
diff --git a/theories/Numbers/NatInt/NZTimesOrder.v b/theories/Numbers/NatInt/NZTimesOrder.v
index 6fc0078c0..4b4516069 100644
--- a/theories/Numbers/NatInt/NZTimesOrder.v
+++ b/theories/Numbers/NatInt/NZTimesOrder.v
@@ -200,11 +200,11 @@ Theorem NZtimes_lt_mono_neg_l : forall p n m : NZ, p < 0 -> (n < m <-> p * m < p
 Proof.
 NZord_induct p.
 intros n m H; false_hyp H NZlt_irrefl.
-intros p H1 _ n m H2. apply NZlt_succ_lt in H2. apply <- NZnle_gt in H2. false_hyp H1 H2.
-intros p H IH n m H1. apply -> NZlt_le_succ in H.
+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_plus_lt n1 m1).
-now le_less. do 2 rewrite <- NZtimes_succ_l. now apply -> IH.
+now apply NZlt_le_incl. do 2 rewrite <- NZtimes_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.
@@ -222,17 +222,17 @@ Qed.
 Theorem NZtimes_le_mono_nonneg_l : forall n m p : NZ, 0 <= p -> n <= m -> p * n <= p * m.
 Proof.
 intros n m p H1 H2. le_elim H1.
-le_elim H2. le_less. now apply -> NZtimes_lt_mono_pos_l.
-le_equal; now rewrite H2.
-le_equal; rewrite <- H1; now do 2 rewrite NZtimes_0_l.
+le_elim H2. apply NZlt_le_incl. now apply -> NZtimes_lt_mono_pos_l.
+apply NZeq_le_incl; now rewrite H2.
+apply NZeq_le_incl; rewrite <- H1; now do 2 rewrite NZtimes_0_l.
 Qed.
 
 Theorem NZtimes_le_mono_nonpos_l : forall n m p : NZ, p <= 0 -> n <= m -> p * m <= p * n.
 Proof.
 intros n m p H1 H2. le_elim H1.
-le_elim H2. le_less. now apply -> NZtimes_lt_mono_neg_l.
-le_equal; now rewrite H2.
-le_equal; rewrite H1; now do 2 rewrite NZtimes_0_l.
+le_elim H2. apply NZlt_le_incl. now apply -> NZtimes_lt_mono_neg_l.
+apply NZeq_le_incl; now rewrite H2.
+apply NZeq_le_incl; rewrite H1; now do 2 rewrite NZtimes_0_l.
 Qed.
 
 Theorem NZtimes_le_mono_nonneg_r : forall n m p : NZ, 0 <= p -> n <= m -> n * p <= m * p.
@@ -272,7 +272,7 @@ Qed.
 
 Theorem NZtimes_le_mono_pos_l : forall n m p : NZ, 0 < p -> (n <= m <-> p * n <= p * m).
 Proof.
-intros n m p H; do 2 rewrite NZle_lt_or_eq.
+intros n m p H; do 2 rewrite NZlt_eq_cases.
 rewrite (NZtimes_lt_mono_pos_l p n m); [assumption |].
 now rewrite -> (NZtimes_cancel_l n m p);
 [intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl |].
@@ -286,7 +286,7 @@ Qed.
 
 Theorem NZtimes_le_mono_neg_l : forall n m p : NZ, p < 0 -> (n <= m <-> p * m <= p * n).
 Proof.
-intros n m p H; do 2 rewrite NZle_lt_or_eq.
+intros n m p H; do 2 rewrite NZlt_eq_cases.
 rewrite (NZtimes_lt_mono_neg_l p n m); [assumption |].
 rewrite -> (NZtimes_cancel_l m n p);
 [intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl |].
@@ -304,7 +304,7 @@ Theorem NZtimes_lt_mono :
 Proof.
 intros n m p q H1 H2 H3 H4.
 apply NZle_lt_trans with (m * p).
-apply NZtimes_le_mono_nonneg_r; [assumption | now le_less].
+apply NZtimes_le_mono_nonneg_r; [assumption | now apply NZlt_le_incl].
 apply -> NZtimes_lt_mono_pos_l; [assumption | now apply NZle_lt_trans with n].
 Qed.
 
@@ -316,10 +316,10 @@ Theorem NZtimes_le_mono :
 Proof.
 intros n m p q H1 H2 H3 H4.
 le_elim H2; le_elim H4.
-le_less; now apply NZtimes_lt_mono.
-rewrite <- H4; apply NZtimes_le_mono_nonneg_r; [assumption | now le_less].
-rewrite <- H2; apply NZtimes_le_mono_nonneg_l; [assumption | now le_less].
-rewrite H2; rewrite H4; now le_equal.
+apply NZlt_le_incl; now apply NZtimes_lt_mono.
+rewrite <- H4; apply NZtimes_le_mono_nonneg_r; [assumption | now apply NZlt_le_incl].
+rewrite <- H2; apply NZtimes_le_mono_nonneg_l; [assumption | now apply NZlt_le_incl].
+rewrite H2; rewrite H4; now apply NZeq_le_incl.
 Qed.
 
 Theorem NZtimes_pos_pos : forall n m : NZ, 0 < n -> 0 < m -> 0 < n * m.
@@ -368,25 +368,46 @@ Proof.
 intros; rewrite NZtimes_comm; now apply NZtimes_nonneg_nonpos.
 Qed.
 
-Theorem NZtimes_eq_0 : forall n m : NZ, n * m == 0 -> n == 0 \/ m == 0.
+Theorem NZlt_1_times_pos : forall n m : NZ, 1 < n -> 0 < m -> 1 < n * m.
 Proof.
-intros n m H; destruct (NZlt_trichotomy n 0) as [H1 | [H1 | H1]];
+intros n m H1 H2. apply -> (NZtimes_lt_mono_pos_r m) in H1.
+rewrite NZtimes_1_l in H1. now apply NZlt_1_l with m.
+assumption.
+Qed.
+
+Theorem NZeq_times_0 : forall n m : NZ, 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]];
 try (now right); try (now left).
 elimtype False; now apply (NZlt_neq 0 (n * m)); [apply NZtimes_neg_neg |].
 elimtype False; now apply (NZlt_neq (n * m) 0); [apply NZtimes_neg_pos |].
 elimtype False; now apply (NZlt_neq (n * m) 0); [apply NZtimes_pos_neg |].
 elimtype False; now apply (NZlt_neq 0 (n * m)); [apply NZtimes_pos_pos |].
+intros [H | H]. now rewrite H, NZtimes_0_l. now rewrite H, NZtimes_0_r.
 Qed.
 
-Theorem NZtimes_neq_0 : forall n m : NZ, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
+Theorem NZneq_times_0 : forall n m : NZ, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
 Proof.
 intros n m; split; intro H.
-intro H1; apply NZtimes_eq_0 in H1. tauto.
+intro H1; apply -> NZeq_times_0 in H1. tauto.
 split; intro H1; rewrite H1 in H;
 (rewrite NZtimes_0_l in H || rewrite NZtimes_0_r in H); now apply H.
 Qed.
 
+Theorem NZeq_times_0_l : forall n m : NZ, n * m == 0 -> m ~= 0 -> n == 0.
+Proof.
+intros n m H1 H2. apply -> NZeq_times_0 in H1. destruct H1 as [H1 | H1].
+assumption. false_hyp H1 H2.
+Qed.
+
+Theorem NZeq_times_0_r : forall n m : NZ, n * m == 0 -> n ~= 0 -> m == 0.
+Proof.
+intros n m H1 H2; apply -> NZeq_times_0 in H1. destruct H1 as [H1 | H1].
+false_hyp H1 H2. assumption.
+Qed.
+
 Theorem NZtimes_pos : forall n m : NZ, 0 < n * m <-> (0 < n /\ 0 < m) \/ (m < 0 /\ n < 0).
 Proof.
 intros n m; split; [intro H | intros [[H1 H2] | [H1 H2]]].
@@ -420,12 +441,12 @@ Qed.
 
 Theorem NZtimes_2_mono_l : forall n m : NZ, n < m -> 1 + (1 + 1) * n < (1 + 1) * m.
 Proof.
-intros n m H. apply -> NZlt_le_succ in H.
+intros n m H. apply <- NZle_succ_l in H.
 apply -> (NZtimes_le_mono_pos_l (S n) m (1 + 1)) in H.
 repeat rewrite NZtimes_plus_distr_r in *; repeat rewrite NZtimes_1_l in *.
 repeat rewrite NZplus_succ_r in *. repeat rewrite NZplus_succ_l in *. rewrite NZplus_0_l.
-now apply <- NZlt_le_succ.
-apply NZplus_pos_pos; now apply NZlt_succ_r.
+now apply -> NZle_succ_l.
+apply NZplus_pos_pos; now apply NZlt_succ_diag_r.
 Qed.
 
 End NZTimesOrderPropFunct.