Clean-up of Zcompare and Zorder

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

2 files changed, 299 insertions, 775 deletions

diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v
index d07f52891..49ab619bc 100644
--- a/theories/ZArith/Zcompare.v
+++ b/theories/ZArith/Zcompare.v
@@ -7,145 +7,92 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $$ i*)
-
 (**********************************************************************)
 (** Binary Integers (Pierre Crégut, CNET, Lannion, France)            *)
 (**********************************************************************)
 
 Require Export BinPos BinInt.
-Require Import Lt Gt Plus Mult.
+Require Import Lt Gt Plus Mult. (* Useless now, for compatibility *)
 
 Local Open Scope Z_scope.
 
 (***************************)
 (** * Comparison on integers *)
 
-Lemma Zcompare_refl : forall n:Z, (n ?= n) = Eq.
-Proof.
- destruct n as [|p|p]; simpl; trivial.
- apply Pcompare_refl.
- apply CompOpp_iff, Pcompare_refl.
-Qed.
-
-Lemma Zcompare_Eq_eq : forall n m:Z, (n ?= m) = Eq -> n = m.
-Proof.
- intros [|x|x] [|y|y] H; simpl in *; try easy; f_equal.
-  now apply Pcompare_Eq_eq.
-  apply CompOpp_iff in H. now apply Pcompare_Eq_eq.
-Qed.
-
 Ltac destr_zcompare :=
- match goal with |- context [Zcompare ?x ?y] =>
+ match goal with |- context [Z.compare ?x ?y] =>
   let H := fresh "H" in
-  case_eq (Zcompare x y); intro H;
-   [generalize (Zcompare_Eq_eq _ _ H); clear H; intro H |
+  case_eq (Z.compare x y); intro H;
+   [generalize (Z.compare_eq _ _ H); clear H; intro H |
     change (x<y)%Z in H |
     change (x>y)%Z in H ]
  end.
 
-Lemma Zcompare_Eq_iff_eq : forall n m:Z, (n ?= m) = Eq <-> n = m.
-Proof.
- intros x y; split; intro E; subst.
- now apply Zcompare_Eq_eq. now apply Zcompare_refl.
-Qed.
-
-Lemma Zcompare_antisym : forall n m:Z, CompOpp (n ?= m) = (m ?= n).
-Proof.
- intros [|x|x] [|y|y]; simpl; try easy; f_equal; apply Pcompare_antisym.
-Qed.
-
-Lemma Zcompare_spec : forall n m, CompareSpec (n=m) (n<m) (m<n) (n ?= m).
-Proof.
- intros.
- destruct (n?=m) as [ ]_eqn:H; constructor; trivial.
- now apply Zcompare_Eq_eq.
- red; now rewrite <- Zcompare_antisym, H.
-Qed.
-
 Lemma Zcompare_Gt_Lt_antisym : forall n m:Z, (n ?= m) = Gt <-> (m ?= n) = Lt.
-Proof.
- intros x y.
- rewrite <- Zcompare_antisym. change Gt with (CompOpp Lt).
- split.
- auto using CompOpp_inj.
- intros; f_equal; auto.
-Qed.
+Proof Z.gt_lt_iff.
+
+Lemma Zcompare_antisym n m : CompOpp (n ?= m) = (m ?= n).
+Proof eq_sym (Z.compare_antisym n m).
 
 (** * Transitivity of comparison *)
 
 Lemma Zcompare_Lt_trans :
   forall n m p:Z, (n ?= m) = Lt -> (m ?= p) = Lt -> (n ?= p) = Lt.
-Proof.
- exact Z.lt_trans.
-Qed.
+Proof Z.lt_trans.
 
 Lemma Zcompare_Gt_trans :
   forall n m p:Z, (n ?= m) = Gt -> (m ?= p) = Gt -> (n ?= p) = Gt.
 Proof.
-  intros n m p Hnm Hmp.
-  apply <- Zcompare_Gt_Lt_antisym.
-  apply -> Zcompare_Gt_Lt_antisym in Hnm.
-  apply -> Zcompare_Gt_Lt_antisym in Hmp.
-  eapply Zcompare_Lt_trans; eauto.
+ intros n m p. change (n > m -> m > p -> n > p).
+ rewrite !Z.gt_lt_iff. intros. now transitivity m.
 Qed.
 
 (** * Comparison and opposite *)
 
-Lemma Zcompare_opp : forall n m, (n ?= m) = (- m ?= - n).
+Lemma Zcompare_opp n m : (n ?= m) = (- m ?= - n).
 Proof.
  symmetry. apply Z.compare_opp.
 Qed.
 
 (** * Comparison first-order specification *)
 
-Lemma Zcompare_Gt_spec :
-  forall n m, (n ?= m) = Gt ->  exists h, n + - m = Zpos h.
+Lemma Zcompare_Gt_spec n m : (n ?= m) = Gt ->  exists h, n + - m = Zpos h.
 Proof.
- intros n m H. rewrite Z.compare_sub in H. unfold Z.sub in H.
+ rewrite Z.compare_sub. unfold Z.sub.
  destruct (n+-m) as [|p|p]; try discriminate. now exists p.
 Qed.
 
 (** * Comparison and addition *)
 
-Lemma Zcompare_plus_compat : forall n m p, (p + n ?= p + m) = (n ?= m).
+Lemma Zcompare_plus_compat n m p : (p + n ?= p + m) = (n ?= m).
 Proof.
- intros. apply Z.add_compare_mono_l.
+ apply Z.add_compare_mono_l.
 Qed.
 
-Lemma Zplus_compare_compat :
-  forall (r:comparison) (n m p q:Z),
-    (n ?= m) = r -> (p ?= q) = r -> (n + p ?= m + q) = r.
+Lemma Zplus_compare_compat (r:comparison) (n m p q:Z) :
+  (n ?= m) = r -> (p ?= q) = r -> (n + p ?= m + q) = r.
 Proof.
- intros r n m p q.
  rewrite (Z.compare_sub n), (Z.compare_sub p), (Z.compare_sub (n+p)).
- unfold Z.sub. rewrite Z.BootStrap.opp_add_distr.
- rewrite <- Z.BootStrap.add_assoc, (Z.BootStrap.add_assoc p).
- rewrite (Z.BootStrap.add_comm p (-m)).
- rewrite <- Z.BootStrap.add_assoc,  (Z.BootStrap.add_assoc n).
+ unfold Z.sub. rewrite Z.opp_add_distr. rewrite Z.add_shuffle1.
  destruct (n+-m), (p+-q); simpl; intros; now subst.
 Qed.
 
-Lemma Zcompare_succ_Gt : forall n:Z, (Zsucc n ?= n) = Gt.
+Lemma Zcompare_succ_Gt n : (Z.succ n ?= n) = Gt.
 Proof.
- intro x; unfold Zsucc; pattern x at 2; rewrite <- (Zplus_0_r x);
-  now rewrite Zcompare_plus_compat.
+ apply Z.lt_gt. apply Z.lt_succ_diag_r.
 Qed.
 
-Lemma Zcompare_Gt_not_Lt : forall n m:Z, (n ?= m) = Gt <-> (n ?= m+1) <> Lt.
+Lemma Zcompare_Gt_not_Lt n m : (n ?= m) = Gt <-> (n ?= m+1) <> Lt.
 Proof.
- intros n m. rewrite 2 (Z.compare_sub n).
- unfold Z.sub. rewrite Z.BootStrap.opp_add_distr.
- rewrite Z.BootStrap.add_assoc.
- destruct (n+-m) as [|[ | | ]|]; simpl; easy'.
+ change (n > m <-> n >= m+1). rewrite Z.gt_lt_iff, Z.ge_le_iff.
+ symmetry. apply Z.le_succ_l.
 Qed.
 
 (** * Successor and comparison *)
 
-Lemma Zcompare_succ_compat : forall n m:Z, (Zsucc n ?= Zsucc m) = (n ?= m).
+Lemma Zcompare_succ_compat n m : (Z.succ n ?= Z.succ m) = (n ?= m).
 Proof.
- intros n m; unfold Zsucc;
-  now rewrite 2 (Zplus_comm _ 1), Zcompare_plus_compat.
+ rewrite <- 2 Z.add_1_l. apply Zcompare_plus_compat.
 Qed.
 
 (** * Multiplication and comparison *)
@@ -153,12 +100,23 @@ Qed.
 Lemma Zcompare_mult_compat :
   forall (p:positive) (n m:Z), (Zpos p * n ?= Zpos p * m) = (n ?= m).
 Proof.
- intros p [|n|n] [|m|m]; simpl; trivial.
-  apply Pmult_compare_mono_l.
-  f_equal. apply Pmult_compare_mono_l.
+ intros p [|n|n] [|m|m]; simpl; trivial; now rewrite Pos.mul_compare_mono_l.
+Qed.
+
+Lemma Zmult_compare_compat_l n m p:
+  p > 0 -> (n ?= m) = (p * n ?= p * m).
+Proof.
+ intros; destruct p; try discriminate.
+ symmetry. apply Zcompare_mult_compat.
 Qed.
 
-(** * Reverting [x ?= y] to trichotomy *)
+Lemma Zmult_compare_compat_r n m p :
+  p > 0 -> (n ?= m) = (n * p ?= m * p).
+Proof.
+ intros; rewrite 2 (Zmult_comm _ p); now apply Zmult_compare_compat_l.
+Qed.
+
+(** * Relating [x ?= y] to [=], [<=], [<], [>=] or [>] *)
 
 Lemma Zcompare_elim :
   forall (c1 c2 c3:Prop) (n m:Z),
@@ -170,9 +128,7 @@ Lemma Zcompare_elim :
                        | Gt => c3
                      end.
 Proof.
- intros c1 c2 c3 x y EQ LT GT; intros.
- case Zcompare_spec; auto.
- intro H. apply GT. red. now rewrite <- Zcompare_antisym, H.
+ intros. case Z.compare_spec; trivial. now rewrite <- Z.gt_lt_iff.
 Qed.
 
 Lemma Zcompare_eq_case :
@@ -183,26 +139,9 @@ Lemma Zcompare_eq_case :
                      | Gt => c3
                    end.
 Proof.
-  intros c1 c2 c3 x y; intros.
-  rewrite H0; rewrite Zcompare_refl.
-  assumption.
+ intros. subst. now rewrite Z.compare_refl.
 Qed.
 
-(** * Decompose an egality between two [?=] relations into 3 implications *)
-
-Lemma Zcompare_egal_dec :
-  forall n m p q:Z,
-    (n < m -> p < q) ->
-    ((n ?= m) = Eq -> (p ?= q) = Eq) ->
-    (n > m -> p > q) -> (n ?= m) = (p ?= q).
-Proof.
-  intros x1 y1 x2 y2.
-  unfold Zgt; unfold Zlt; case (x1 ?= y1); case (x2 ?= y2);
-    auto with arith; symmetry; auto with arith.
-Qed.
-
-(** * Relating [x ?= y] to [Zle], [Zlt], [Zge] or [Zgt] *)
-
 Lemma Zle_compare :
   forall n m:Z,
     n <= m -> match n ?= m with
@@ -211,7 +150,7 @@ Lemma Zle_compare :
 		| Gt => False
               end.
 Proof.
-  intros x y; unfold Zle; elim (x ?= y); auto with arith.
+  intros. case Z.compare_spec; trivial; Z.order.
 Qed.
 
 Lemma Zlt_compare :
@@ -222,8 +161,7 @@ Lemma Zlt_compare :
               | Gt => False
             end.
 Proof.
-  intros x y; unfold Zlt in |- *; elim (x ?= y); intros;
-    discriminate || trivial with arith.
+  intros x y H; now rewrite H.
 Qed.
 
 Lemma Zge_compare :
@@ -234,7 +172,7 @@ Lemma Zge_compare :
 		| Gt => True
               end.
 Proof.
-  intros x y; unfold Zge; elim (x ?= y); auto.
+  intros. now case Z.compare_spec.
 Qed.
 
 Lemma Zgt_compare :
@@ -245,28 +183,15 @@ Lemma Zgt_compare :
                | Gt => True
              end.
 Proof.
-  intros x y; unfold Zgt; now elim (x ?= y).
+  intros x y H; now rewrite H.
 Qed.
 
-(*********************)
-(** * Other properties *)
-
-Lemma Zmult_compare_compat_l :
-  forall n m p:Z, p > 0 -> (n ?= m) = (p * n ?= p * m).
-Proof.
-  intros x y z H; destruct z.
-  discriminate H.
-  rewrite Zcompare_mult_compat; reflexivity.
-  discriminate H.
-Qed.
-
-Lemma Zmult_compare_compat_r :
-  forall n m p:Z, p > 0 -> (n ?= m) = (n * p ?= m * p).
-Proof.
-  intros x y z H; rewrite 2 (Zmult_comm _ z);
-    apply Zmult_compare_compat_l; assumption.
-Qed.
+(** Compatibility notations *)
 
+Notation Zcompare_refl := Z.compare_refl (only parsing).
+Notation Zcompare_Eq_eq := Z.compare_eq (only parsing).
+Notation Zcompare_Eq_iff_eq := Z.compare_eq_iff (only parsing).
+Notation Zcompare_spec := Z.compare_spec (only parsing).
 Notation Zmin_l := Z.min_l (only parsing).
 Notation Zmin_r := Z.min_r (only parsing).
 Notation Zmax_l := Z.max_l (only parsing).
@@ -277,3 +202,4 @@ Notation Zsgn_0 := Z.sgn_null (only parsing).
 Notation Zsgn_1 := Z.sgn_pos (only parsing).
 Notation Zsgn_m1 := Z.sgn_neg (only parsing).
 
+(** Not kept: Zcompare_egal_dec *)
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index fcac8c33a..52f2b67ea 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -8,328 +8,181 @@
 (************************************************************************)
 (** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
 
-Require Import BinPos.
-Require Import BinInt.
-Require Import Arith_base.
-Require Import Decidable.
-Require Import Zcompare.
+Require Import BinPos BinInt Decidable Zcompare.
+Require Import Arith_base. (* Useless now, for compatibility *)
 
-Open Local Scope Z_scope.
-
-Implicit Types x y z : Z.
+Local Open Scope Z_scope.
 
 (*********************************************************)
 (** Properties of the order relations on binary integers *)
 
 (** * Trichotomy *)
 
-Theorem Ztrichotomy_inf : forall n m:Z, {n < m} + {n = m} + {n > m}.
+Theorem Ztrichotomy_inf n m : {n < m} + {n = m} + {n > m}.
 Proof.
-  unfold Zgt, Zlt in |- *; intros m n; assert (H := refl_equal (m ?= n)).
-  set (x := m ?= n) in H at 2 |- *.
-  destruct x;
-    [ left; right; rewrite Zcompare_Eq_eq with (1 := H) | left; left | right ];
-    reflexivity.
-Qed.
+  unfold ">", "<". generalize (Z.compare_eq n m).
+  destruct (n ?= m); [ left; right | left; left | right]; auto.
+Defined.
 
-Theorem Ztrichotomy : forall n m:Z, n < m \/ n = m \/ n > m.
+Theorem Ztrichotomy n m : n < m \/ n = m \/ n > m.
 Proof.
-  intros m n; destruct (Ztrichotomy_inf m n) as [[Hlt| Heq]| Hgt];
-    [ left | right; left | right; right ]; assumption.
+  rewrite Z.gt_lt_iff. apply Z.lt_trichotomy.
 Qed.
 
 (**********************************************************************)
 (** * Decidability of equality and order on Z *)
 
-Theorem dec_eq : forall n m:Z, decidable (n = m).
-Proof.
-  intros x y; unfold decidable in |- *; elim (Zcompare_Eq_iff_eq x y);
-    intros H1 H2; elim (Dcompare (x ?= y));
-      [ tauto
-	| intros H3; right; unfold not in |- *; intros H4; elim H3; rewrite (H2 H4);
-	  intros H5; discriminate H5 ].
-Qed.
+Notation dec_eq := Z.eq_decidable (only parsing).
+Notation dec_Zle := Z.le_decidable (only parsing).
+Notation dec_Zlt := Z.lt_decidable (only parsing).
 
-Theorem dec_Zne : forall n m:Z, decidable (Zne n m).
+Theorem dec_Zne n m : decidable (Zne n m).
 Proof.
-  intros x y; unfold decidable, Zne in |- *; elim (Zcompare_Eq_iff_eq x y).
-  intros H1 H2; elim (Dcompare (x ?= y));
-    [ right; rewrite H1; auto
-      | left; unfold not in |- *; intro; absurd ((x ?= y) = Eq);
-	[ elim H; intros HR; rewrite HR; discriminate | auto ] ].
+  destruct (Z.eq_decidable n m); [right|left]; subst; auto.
 Qed.
 
-Theorem dec_Zle : forall n m:Z, decidable (n <= m).
+Theorem dec_Zgt n m : decidable (n > m).
 Proof.
-  intros x y; unfold decidable, Zle in |- *; elim (x ?= y);
-    [ left; discriminate
-      | left; discriminate
-      | right; unfold not in |- *; intros H; apply H; trivial with arith ].
+  destruct (Z.lt_decidable m n); [left|right]; rewrite Z.gt_lt_iff; auto.
 Qed.
 
-Theorem dec_Zgt : forall n m:Z, decidable (n > m).
+Theorem dec_Zge n m : decidable (n >= m).
 Proof.
-  intros x y; unfold decidable, Zgt in |- *; elim (x ?= y);
-    [ right; discriminate | right; discriminate | auto with arith ].
+  destruct (Z.le_decidable m n); [left|right]; rewrite Z.ge_le_iff; auto.
 Qed.
 
-Theorem dec_Zge : forall n m:Z, decidable (n >= m).
+Theorem not_Zeq n m : n <> m -> n < m \/ m < n.
 Proof.
-  intros x y; unfold decidable, Zge in |- *; elim (x ?= y);
-    [ left; discriminate
-      | right; unfold not in |- *; intros H; apply H; trivial with arith
-      | left; discriminate ].
-Qed.
-
-Theorem dec_Zlt : forall n m:Z, decidable (n < m).
-Proof.
-  intros x y; unfold decidable, Zlt in |- *; elim (x ?= y);
-    [ right; discriminate | auto with arith | right; discriminate ].
-Qed.
-
-Theorem not_Zeq : forall n m:Z, n <> m -> n < m \/ m < n.
-Proof.
-  intros x y; elim (Dcompare (x ?= y));
-    [ intros H1 H2; absurd (x = y);
-      [ assumption | elim (Zcompare_Eq_iff_eq x y); auto with arith ]
-      | unfold Zlt in |- *; intros H; elim H; intros H1;
-	[ auto with arith
-	  | right; elim (Zcompare_Gt_Lt_antisym x y); auto with arith ] ].
+  apply Z.lt_gt_cases.
 Qed.
 
 (** * Relating strict and large orders *)
 
-Lemma Zgt_lt : forall n m:Z, n > m -> m < n.
-Proof.
-  unfold Zgt, Zlt in |- *; intros m n H; elim (Zcompare_Gt_Lt_antisym m n);
-    auto with arith.
-Qed.
-
-Lemma Zlt_gt : forall n m:Z, n < m -> m > n.
-Proof.
-  unfold Zgt, Zlt in |- *; intros m n H; elim (Zcompare_Gt_Lt_antisym n m);
-    auto with arith.
-Qed.
+Notation Zgt_lt := Z.gt_lt (only parsing).
+Notation Zlt_gt := Z.lt_gt (only parsing).
+Notation Zge_le := Z.ge_le (only parsing).
+Notation Zle_ge := Z.le_ge (only parsing).
+Notation Zgt_iff_lt := Z.gt_lt_iff (only parsing).
+Notation Zge_iff_le := Z.ge_le_iff (only parsing).
 
-Lemma Zge_le : forall n m:Z, n >= m -> m <= n.
+Lemma Zle_not_lt n m : n <= m -> ~ m < n.
 Proof.
-  intros m n; change (~ m < n -> ~ n > m) in |- *; unfold not in |- *;
-    intros H1 H2; apply H1; apply Zgt_lt; assumption.
+ apply Z.le_ngt.
 Qed.
 
-Lemma Zle_ge : forall n m:Z, n <= m -> m >= n.
+Lemma Zlt_not_le n m : n < m -> ~ m <= n.
 Proof.
-  intros m n; change (~ m > n -> ~ n < m) in |- *; unfold not in |- *;
-    intros H1 H2; apply H1; apply Zlt_gt; assumption.
+ apply Z.lt_nge.
 Qed.
 
-Lemma Zle_not_gt : forall n m:Z, n <= m -> ~ n > m.
+Lemma Zle_not_gt n m : n <= m -> ~ n > m.
 Proof.
   trivial.
 Qed.
 
-Lemma Zgt_not_le : forall n m:Z, n > m -> ~ n <= m.
+Lemma Zgt_not_le n m : n > m -> ~ n <= m.
 Proof.
-  intros n m H1 H2; apply H2; assumption.
+  rewrite Z.gt_lt_iff. apply Z.lt_nge.
 Qed.
 
-Lemma Zle_not_lt : forall n m:Z, n <= m -> ~ m < n.
+Lemma Znot_ge_lt n m : ~ n >= m -> n < m.
 Proof.
-  intros n m H1 H2.
-  assert (H3 := Zlt_gt _ _ H2).
-  apply Zle_not_gt with n m; assumption.
+  rewrite Z.ge_le_iff. apply Z.nle_gt.
 Qed.
 
-Lemma Zlt_not_le : forall n m:Z, n < m -> ~ m <= n.
-Proof.
-  intros n m H1 H2.
-  apply Zle_not_lt with m n; assumption.
-Qed.
-
-Lemma Znot_ge_lt : forall n m:Z, ~ n >= m -> n < m.
-Proof.
-  unfold Zge, Zlt in |- *; intros x y H; apply dec_not_not;
-    [ exact (dec_Zlt x y) | assumption ].
-Qed.
-
-Lemma Znot_lt_ge : forall n m:Z, ~ n < m -> n >= m.
-Proof.
-  unfold Zlt, Zge in |- *; auto with arith.
-Qed.
-
-Lemma Znot_gt_le : forall n m:Z, ~ n > m -> n <= m.
+Lemma Znot_lt_ge n m : ~ n < m -> n >= m.
 Proof.
   trivial.
 Qed.
 
-Lemma Znot_le_gt : forall n m:Z, ~ n <= m -> n > m.
-Proof.
-  unfold Zle, Zgt in |- *; intros x y H; apply dec_not_not;
-    [ exact (dec_Zgt x y) | assumption ].
-Qed.
-
-Lemma Zge_iff_le : forall n m:Z, n >= m <-> m <= n.
+Lemma Znot_gt_le n m: ~ n > m -> n <= m.
 Proof.
-  intros x y; intros. split. intro. apply Zge_le. assumption.
-  intro. apply Zle_ge. assumption.
+  trivial.
 Qed.
 
-Lemma Zgt_iff_lt : forall n m:Z, n > m <-> m < n.
+Lemma Znot_le_gt n m : ~ n <= m -> n > m.
 Proof.
-  intros x y. split. intro. apply Zgt_lt. assumption.
-  intro. apply Zlt_gt. assumption.
+  rewrite Z.gt_lt_iff. apply Z.nle_gt.
 Qed.
 
 (** * Equivalence and order properties *)
 
 (** Reflexivity *)
 
-Lemma Zle_refl : forall n:Z, n <= n.
-Proof.
-  intros n; unfold Zle in |- *; rewrite (Zcompare_refl n); discriminate.
-Qed.
-
-Lemma Zeq_le : forall n m:Z, n = m -> n <= m.
-Proof.
-  intros; rewrite H; apply Zle_refl.
-Qed.
+Notation Zle_refl := Z.le_refl (only parsing).
+Notation Zeq_le := Z.eq_le_incl (only parsing).
 
-Hint Resolve Zle_refl: zarith.
+Hint Resolve Z.le_refl: zarith.
 
 (** Antisymmetry *)
 
-Lemma Zle_antisym : forall n m:Z, n <= m -> m <= n -> n = m.
-Proof.
-  intros n m H1 H2; destruct (Ztrichotomy n m) as [Hlt| [Heq| Hgt]].
-  absurd (m > n); [ apply Zle_not_gt | apply Zlt_gt ]; assumption.
-  assumption.
-  absurd (n > m); [ apply Zle_not_gt | idtac ]; assumption.
-Qed.
+Notation Zle_antisym := Z.le_antisymm (only parsing).
 
 (** Asymmetry *)
 
-Lemma Zgt_asym : forall n m:Z, n > m -> ~ m > n.
-Proof.
-  unfold Zgt in |- *; intros n m H; elim (Zcompare_Gt_Lt_antisym n m);
-    intros H1 H2; rewrite H1; [ discriminate | assumption ].
-Qed.
+Notation Zlt_asym := Z.lt_asymm (only parsing).
 
-Lemma Zlt_asym : forall n m:Z, n < m -> ~ m < n.
+Lemma Zgt_asym n m : n > m -> ~ m > n.
 Proof.
-  intros n m H H1; assert (H2 : m > n). apply Zlt_gt; assumption.
-  assert (H3 : n > m). apply Zlt_gt; assumption.
-  apply Zgt_asym with m n; assumption.
+  rewrite !Z.gt_lt_iff. apply Z.lt_asymm.
 Qed.
 
 (** Irreflexivity *)
 
-Lemma Zgt_irrefl : forall n:Z, ~ n > n.
-Proof.
-  intros n H; apply (Zgt_asym n n H H).
-Qed.
-
-Lemma Zlt_irrefl : forall n:Z, ~ n < n.
-Proof.
-  intros n H; apply (Zlt_asym n n H H).
-Qed.
+Notation Zlt_irrefl := Z.lt_irrefl (only parsing).
+Notation Zlt_not_eq := Z.lt_neq (only parsing).
 
-Lemma Zlt_not_eq : forall n m:Z, n < m -> n <> m.
+Lemma Zgt_irrefl n : ~ n > n.
 Proof.
-  unfold not in |- *; intros x y H H0.
-  rewrite H0 in H.
-  apply (Zlt_irrefl _ H).
+  rewrite Z.gt_lt_iff. apply Z.lt_irrefl.
 Qed.
 
 (** Large = strict or equal *)
 
-Lemma Zlt_le_weak : forall n m:Z, n < m -> n <= m.
-Proof.
-  intros n m Hlt; apply Znot_gt_le; apply Zgt_asym; apply Zlt_gt; assumption.
-Qed.
-
-Lemma Zle_lt_or_eq : forall n m:Z, n <= m -> n < m \/ n = m.
-Proof.
-  intros n m H; destruct (Ztrichotomy n m) as [Hlt| [Heq| Hgt]];
-    [ left; assumption
-      | right; assumption
-      | absurd (n > m); [ apply Zle_not_gt | idtac ]; assumption ].
-Qed.
+Notation Zlt_le_weak := Z.lt_le_incl (only parsing).
+Notation Zle_lt_or_eq_iff := Z.lt_eq_cases (only parsing).
 
-Lemma Zle_lt_or_eq_iff : forall n m, n <= m <-> n < m \/ n = m.
+Lemma Zle_lt_or_eq n m : n <= m -> n < m \/ n = m.
 Proof.
-  unfold Zle, Zlt. intros.
-  generalize (Zcompare_Eq_iff_eq n m).
-  destruct (n ?= m); intuition; discriminate.
+  apply Z.lt_eq_cases.
 Qed.
 
 (** Dichotomy *)
 
-Lemma Zle_or_lt : forall n m:Z, n <= m \/ m < n.
-Proof.
-  intros n m; destruct (Ztrichotomy n m) as [Hlt| [Heq| Hgt]];
-    [ left; apply Znot_gt_le; intro Hgt; assert (Hgt' := Zlt_gt _ _ Hlt);
-      apply Zgt_asym with m n; assumption
-      | left; rewrite Heq; apply Zle_refl
-      | right; apply Zgt_lt; assumption ].
-Qed.
+Notation Zle_or_lt := Z.le_gt_cases (only parsing).
 
 (** Transitivity of strict orders *)
 
-Lemma Zgt_trans : forall n m p:Z, n > m -> m > p -> n > p.
-Proof.
-  exact Zcompare_Gt_trans.
-Qed.
+Notation Zlt_trans := Z.lt_trans (only parsing).
 
-Lemma Zlt_trans : forall n m p:Z, n < m -> m < p -> n < p.
-Proof.
-  exact Zcompare_Lt_trans.
-Qed.
+Lemma Zgt_trans : forall n m p:Z, n > m -> m > p -> n > p.
+Proof Zcompare_Gt_trans.
 
 (** Mixed transitivity *)
 
-Lemma Zle_gt_trans : forall n m p:Z, m <= n -> m > p -> n > p.
-Proof.
-  intros n m p H1 H2; destruct (Zle_lt_or_eq m n H1) as [Hlt| Heq];
-    [ apply Zgt_trans with m; [ apply Zlt_gt; assumption | assumption ]
-      | rewrite <- Heq; assumption ].
-Qed.
+Notation Zlt_le_trans := Z.lt_le_trans (only parsing).
+Notation Zle_lt_trans := Z.le_lt_trans (only parsing).
 
-Lemma Zgt_le_trans : forall n m p:Z, n > m -> p <= m -> n > p.
+Lemma Zle_gt_trans n m p : m <= n -> m > p -> n > p.
 Proof.
-  intros n m p H1 H2; destruct (Zle_lt_or_eq p m H2) as [Hlt| Heq];
-    [ apply Zgt_trans with m; [ assumption | apply Zlt_gt; assumption ]
-      | rewrite Heq; assumption ].
+  rewrite !Z.gt_lt_iff. Z.order.
 Qed.
 
-Lemma Zlt_le_trans : forall n m p:Z, n < m -> m <= p -> n < p.
-  intros n m p H1 H2; apply Zgt_lt; apply Zle_gt_trans with (m := m);
-    [ assumption | apply Zlt_gt; assumption ].
-Qed.
-
-Lemma Zle_lt_trans : forall n m p:Z, n <= m -> m < p -> n < p.
+Lemma Zgt_le_trans n m p : n > m -> p <= m -> n > p.
 Proof.
-  intros n m p H1 H2; apply Zgt_lt; apply Zgt_le_trans with (m := m);
-    [ apply Zlt_gt; assumption | assumption ].
+  rewrite !Z.gt_lt_iff. Z.order.
 Qed.
 
 (** Transitivity of large orders *)
 
-Lemma Zle_trans : forall n m p:Z, n <= m -> m <= p -> n <= p.
-Proof.
-  intros n m p H1 H2; apply Znot_gt_le.
-  intro Hgt; apply Zle_not_gt with n m. assumption.
-  exact (Zgt_le_trans n p m Hgt H2).
-Qed.
+Notation Zle_trans := Z.le_trans (only parsing).
 
-Lemma Zge_trans : forall n m p:Z, n >= m -> m >= p -> n >= p.
+Lemma Zge_trans n m p : n >= m -> m >= p -> n >= p.
 Proof.
-  intros n m p H1 H2.
-  apply Zle_ge.
-  apply Zle_trans with m; apply Zge_le; trivial.
+  rewrite !Z.ge_le_iff. Z.order.
 Qed.
 
-Hint Resolve Zle_trans: zarith.
-
+Hint Resolve Z.le_trans: zarith.
 
 (** * Compatibility of order and operations on Z *)
 
@@ -337,705 +190,450 @@ Hint Resolve Zle_trans: zarith.
 
 (** Compatibility of successor wrt to order *)
 
-Lemma Zsucc_le_compat : forall n m:Z, m <= n -> Zsucc m <= Zsucc n.
+Lemma Zsucc_le_compat n m : m <= n -> Z.succ m <= Z.succ n.
 Proof.
-  unfold Zle, not in |- *; intros m n H1 H2; apply H1;
-    rewrite <- (Zcompare_plus_compat n m 1); do 2 rewrite (Zplus_comm 1);
-      exact H2.
+  apply Z.succ_le_mono.
 Qed.
 
-Lemma Zsucc_gt_compat : forall n m:Z, m > n -> Zsucc m > Zsucc n.
+Lemma Zsucc_lt_compat n m : n < m -> Z.succ n < Z.succ m.
 Proof.
-  unfold Zgt in |- *; intros n m H; rewrite Zcompare_succ_compat;
-    auto with arith.
+  apply Z.succ_lt_mono.
 Qed.
 
-Lemma Zsucc_lt_compat : forall n m:Z, n < m -> Zsucc n < Zsucc m.
+Lemma Zsucc_gt_compat n m : m > n -> Z.succ m > Z.succ n.
 Proof.
-  intros n m H; apply Zgt_lt; apply Zsucc_gt_compat; apply Zlt_gt; assumption.
+  rewrite !Z.gt_lt_iff. apply Z.succ_lt_mono.
 Qed.
 
 Hint Resolve Zsucc_le_compat: zarith.
 
 (** Simplification of successor wrt to order *)
 
-Lemma Zsucc_gt_reg : forall n m:Z, Zsucc m > Zsucc n -> m > n.
+Lemma Zsucc_gt_reg n m : Z.succ m > Z.succ n -> m > n.
 Proof.
-  unfold Zsucc, Zgt in |- *; intros n p;
-    do 2 rewrite (fun m:Z => Zplus_comm m 1);
-      rewrite (Zcompare_plus_compat p n 1); trivial with arith.
+  rewrite !Z.gt_lt_iff. apply Z.succ_lt_mono.
 Qed.
 
-Lemma Zsucc_le_reg : forall n m:Z, Zsucc m <= Zsucc n -> m <= n.
+Lemma Zsucc_le_reg n m : Z.succ m <= Z.succ n -> m <= n.
 Proof.
-  unfold Zle, not in |- *; intros m n H1 H2; apply H1; unfold Zsucc in |- *;
-    do 2 rewrite <- (Zplus_comm 1); rewrite (Zcompare_plus_compat n m 1);
-      assumption.
+  apply Z.succ_le_mono.
 Qed.
 
-Lemma Zsucc_lt_reg : forall n m:Z, Zsucc n < Zsucc m -> n < m.
+Lemma Zsucc_lt_reg n m : Z.succ n < Z.succ m -> n < m.
 Proof.
-  intros n m H; apply Zgt_lt; apply Zsucc_gt_reg; apply Zlt_gt; assumption.
+  apply Z.succ_lt_mono.
 Qed.
 
 (** Special base instances of order *)
 
-Lemma Zgt_succ : forall n:Z, Zsucc n > n.
-Proof.
-  exact Zcompare_succ_Gt.
-Qed.
-
-Lemma Znot_le_succ : forall n:Z, ~ Zsucc n <= n.
-Proof.
-  intros n; apply Zgt_not_le; apply Zgt_succ.
-Qed.
+Notation Zlt_succ := Z.lt_succ_diag_r (only parsing).
+Notation Zlt_pred := Z.lt_pred_l (only parsing).
 
-Lemma Zlt_succ : forall n:Z, n < Zsucc n.
+Lemma Zgt_succ n : Z.succ n > n.
 Proof.
-  intro n; apply Zgt_lt; apply Zgt_succ.
+  apply Z.lt_gt, Z.lt_succ_diag_r.
 Qed.
 
-Lemma Zlt_pred : forall n:Z, Zpred n < n.
+Lemma Znot_le_succ n : ~ Z.succ n <= n.
 Proof.
-  intros n; apply Zsucc_lt_reg; rewrite <- Zsucc_pred; apply Zlt_succ.
+  apply Z.lt_nge, Z.lt_succ_diag_r.
 Qed.
 
 (** Relating strict and large order using successor or predecessor *)
 
-Lemma Zgt_le_succ : forall n m:Z, m > n -> Zsucc n <= m.
-Proof.
-  unfold Zgt, Zle in |- *; intros n p H; elim (Zcompare_Gt_not_Lt p n);
-    intros H1 H2; unfold not in |- *; intros H3; unfold not in H1;
-      apply H1;
-	[ assumption
-	  | elim (Zcompare_Gt_Lt_antisym (n + 1) p); intros H4 H5; apply H4; exact H3 ].
-Qed.
+Notation Zlt_succ_r := Z.lt_succ_r (only parsing).
+Notation Zle_succ_l := Z.le_succ_l (only parsing).
 
-Lemma Zle_gt_succ : forall n m:Z, n <= m -> Zsucc m > n.
+Lemma Zgt_le_succ n m : m > n -> Z.succ n <= m.
 Proof.
-  intros n p H; apply Zgt_le_trans with p.
-  apply Zgt_succ.
-  assumption.
+  rewrite Z.gt_lt_iff. apply Z.le_succ_l.
 Qed.
 
-Lemma Zle_lt_succ : forall n m:Z, n <= m -> n < Zsucc m.
+Lemma Zle_gt_succ n m : n <= m -> Z.succ m > n.
 Proof.
-  intros n m H; apply Zgt_lt; apply Zle_gt_succ; assumption.
+  rewrite Z.gt_lt_iff. apply Z.lt_succ_r.
 Qed.
 
-Lemma Zlt_le_succ : forall n m:Z, n < m -> Zsucc n <= m.
+Lemma Zle_lt_succ n m : n <= m -> n < Z.succ m.
 Proof.
-  intros n p H; apply Zgt_le_succ; apply Zlt_gt; assumption.
+  apply Z.lt_succ_r.
 Qed.
 
-Lemma Zgt_succ_le : forall n m:Z, Zsucc m > n -> n <= m.
+Lemma Zlt_le_succ n m : n < m -> Z.succ n <= m.
 Proof.
-  intros n p H; apply Zsucc_le_reg; apply Zgt_le_succ; assumption.
+  apply Z.le_succ_l.
 Qed.
 
-Lemma Zlt_succ_le : forall n m:Z, n < Zsucc m -> n <= m.
+Lemma Zgt_succ_le n m : Z.succ m > n -> n <= m.
 Proof.
-  intros n m H; apply Zgt_succ_le; apply Zlt_gt; assumption.
+  rewrite Z.gt_lt_iff. apply Z.lt_succ_r.
 Qed.
 
-Lemma Zle_succ_gt : forall n m:Z, Zsucc n <= m -> m > n.
+Lemma Zlt_succ_le n m : n < Z.succ m -> n <= m.
 Proof.
-  intros n m H; apply Zle_gt_trans with (m := Zsucc n);
-    [ assumption | apply Zgt_succ ].
+  apply Z.lt_succ_r.
 Qed.
 
-Notation Zlt_succ_r := Z.lt_succ_r (only parsing).
-
-Lemma Zle_succ_l : forall n m, Zsucc n <= m <-> n < m.
+Lemma Zle_succ_gt n m : Z.succ n <= m -> m > n.
 Proof.
- intros. split; intros H.
- rewrite (Zsucc_pred m). apply Zle_lt_succ, Zsucc_le_reg.
- now rewrite <- Zsucc_pred.
- now apply Zlt_le_succ.
+  rewrite Z.gt_lt_iff. apply Z.le_succ_l.
 Qed.
 
 (** Weakening order *)
 
-Lemma Zle_succ : forall n:Z, n <= Zsucc n.
-Proof.
-  intros n; apply Zgt_succ_le; apply Zgt_trans with (m := Zsucc n);
-    apply Zgt_succ.
-Qed.
+Notation Zle_succ := Z.le_succ_diag_r (only parsing).
+Notation Zle_pred := Z.le_pred_l (only parsing).
+Notation Zlt_lt_succ := Z.lt_lt_succ_r (only parsing).
+Notation Zle_le_succ := Z.le_le_succ_r (only parsing).
 
-Hint Resolve Zle_succ: zarith.
-
-Lemma Zle_pred : forall n:Z, Zpred n <= n.
-Proof.
-  intros n; pattern n at 2 in |- *; rewrite Zsucc_pred; apply Zle_succ.
-Qed.
-
-Lemma Zlt_lt_succ : forall n m:Z, n < m -> n < Zsucc m.
-  intros n m H; apply Zgt_lt; apply Zgt_trans with (m := m);
-    [ apply Zgt_succ | apply Zlt_gt; assumption ].
-Qed.
-
-Lemma Zle_le_succ : forall n m:Z, n <= m -> n <= Zsucc m.
+Lemma Zle_succ_le n m : Z.succ n <= m -> n <= m.
 Proof.
-  intros x y H.
-  apply Zle_trans with y; trivial with zarith.
-Qed.
-
-Lemma Zle_succ_le : forall n m:Z, Zsucc n <= m -> n <= m.
-Proof.
-  intros n m H; apply Zle_trans with (m := Zsucc n);
-    [ apply Zle_succ | assumption ].
+  intros. now apply Z.lt_le_incl, Z.le_succ_l.
 Qed.
 
+Hint Resolve Z.le_succ_diag_r: zarith.
 Hint Resolve Zle_le_succ: zarith.
 
 (** Relating order wrt successor and order wrt predecessor *)
 
-Lemma Zgt_succ_pred : forall n m:Z, m > Zsucc n -> Zpred m > n.
+Lemma Zgt_succ_pred n m : m > Z.succ n -> Z.pred m > n.
 Proof.
-  unfold Zgt, Zsucc, Zpred in |- *; intros n p H;
-    rewrite <- (fun x y => Zcompare_plus_compat x y 1);
-      rewrite (Zplus_comm p); rewrite Zplus_assoc;
-	rewrite (fun x => Zplus_comm x n); simpl in |- *;
-	  assumption.
+  rewrite !Z.gt_lt_iff. apply Z.lt_succ_lt_pred.
 Qed.
 
-Lemma Zlt_succ_pred : forall n m:Z, Zsucc n < m -> n < Zpred m.
+Lemma Zlt_succ_pred n m : Z.succ n < m -> n < Z.pred m.
 Proof.
-  intros n p H; apply Zsucc_lt_reg; rewrite <- Zsucc_pred; assumption.
+  apply Z.lt_succ_lt_pred.
 Qed.
 
 (** Relating strict order and large order on positive *)
 
-Lemma Zlt_0_le_0_pred : forall n:Z, 0 < n -> 0 <= Zpred n.
+Lemma Zlt_0_le_0_pred n : 0 < n -> 0 <= Z.pred n.
 Proof.
-  intros x H.
-  rewrite (Zsucc_pred x) in H.
-  apply Zgt_succ_le.
-  apply Zlt_gt.
-  assumption.
+  apply Z.lt_le_pred.
 Qed.
 
-Lemma Zgt_0_le_0_pred : forall n:Z, n > 0 -> 0 <= Zpred n.
+Lemma Zgt_0_le_0_pred n : n > 0 -> 0 <= Z.pred n.
 Proof.
-  intros; apply Zlt_0_le_0_pred; apply Zgt_lt. assumption.
+  rewrite Z.gt_lt_iff. apply Z.lt_le_pred.
 Qed.
 
-
 (** Special cases of ordered integers *)
 
-Lemma Zlt_0_1 : 0 < 1.
-Proof.
-  change (0 < Zsucc 0) in |- *. apply Zlt_succ.
-Qed.
-
-Lemma Zle_0_1 : 0 <= 1.
-Proof.
-  change (0 <= Zsucc 0) in |- *. apply Zle_succ.
-Qed.
+Notation Zlt_0_1 := Z.lt_0_1 (only parsing).
+Notation Zle_0_1 := Z.le_0_1 (only parsing).
 
 Lemma Zle_neg_pos : forall p q:positive, Zneg p <= Zpos q.
 Proof.
-  intros p; red in |- *; simpl in |- *; red in |- *; intros H; discriminate.
+  easy.
 Qed.
 
 Lemma Zgt_pos_0 : forall p:positive, Zpos p > 0.
 Proof.
-  unfold Zgt in |- *; trivial.
+  easy.
 Qed.
 
 (* weaker but useful (in [Zpower] for instance) *)
 Lemma Zle_0_pos : forall p:positive, 0 <= Zpos p.
 Proof.
-  intro; unfold Zle in |- *; discriminate.
+ easy.
 Qed.
 
 Lemma Zlt_neg_0 : forall p:positive, Zneg p < 0.
 Proof.
-  unfold Zlt in |- *; trivial.
+ easy.
 Qed.
 
-Lemma Zle_0_nat : forall n:nat, 0 <= Z_of_nat n.
+Lemma Zle_0_nat : forall n:nat, 0 <= Z.of_nat n.
 Proof.
-  simple induction n; simpl in |- *; intros;
-    [ apply Zle_refl | unfold Zle in |- *; simpl in |- *; discriminate ].
+  induction n; simpl; intros. apply Z.le_refl. easy.
 Qed.
 
 Hint Immediate Zeq_le: zarith.
 
-(** Transitivity using successor *)
-
-Lemma Zgt_trans_succ : forall n m p:Z, Zsucc n > m -> m > p -> n > p.
-Proof.
-  intros n m p H1 H2; apply Zle_gt_trans with (m := m);
-    [ apply Zgt_succ_le; assumption | assumption ].
-Qed.
-
 (** Derived lemma *)
 
-Lemma Zgt_succ_gt_or_eq : forall n m:Z, Zsucc n > m -> n > m \/ m = n.
+Lemma Zgt_succ_gt_or_eq n m : Z.succ n > m -> n > m \/ m = n.
 Proof.
-  intros n m H.
-  assert (Hle : m <= n).
-  apply Zgt_succ_le; assumption.
-  destruct (Zle_lt_or_eq _ _ Hle) as [Hlt| Heq].
-  left; apply Zlt_gt; assumption.
-  right; assumption.
+  rewrite !Z.gt_lt_iff. intros. now apply Z.lt_eq_cases, Z.lt_succ_r.
 Qed.
 
 (** ** Addition *)
 (** Compatibility of addition wrt to order *)
 
-Lemma Zplus_gt_compat_l : forall n m p:Z, n > m -> p + n > p + m.
-Proof.
-  unfold Zgt in |- *; intros n m p H; rewrite (Zcompare_plus_compat n m p);
-    assumption.
-Qed.
-
-Lemma Zplus_gt_compat_r : forall n m p:Z, n > m -> n + p > m + p.
-Proof.
-  intros n m p H; rewrite (Zplus_comm n p); rewrite (Zplus_comm m p);
-    apply Zplus_gt_compat_l; trivial.
-Qed.
+Notation Zplus_lt_le_compat := Z.add_lt_le_mono (only parsing).
+Notation Zplus_le_lt_compat := Z.add_le_lt_mono (only parsing).
+Notation Zplus_le_compat := Z.add_le_mono (only parsing).
+Notation Zplus_lt_compat := Z.add_lt_mono (only parsing).
 
-Lemma Zplus_le_compat_l : forall n m p:Z, n <= m -> p + n <= p + m.
+Lemma Zplus_gt_compat_l n m p : n > m -> p + n > p + m.
 Proof.
-  intros n m p; unfold Zle, not in |- *; intros H1 H2; apply H1;
-    rewrite <- (Zcompare_plus_compat n m p); assumption.
+  rewrite !Z.gt_lt_iff. apply Z.add_lt_mono_l.
 Qed.
 
-Lemma Zplus_le_compat_r : forall n m p:Z, n <= m -> n + p <= m + p.
+Lemma Zplus_gt_compat_r n m p : n > m -> n + p > m + p.
 Proof.
-  intros a b c; do 2 rewrite (fun n:Z => Zplus_comm n c);
-    exact (Zplus_le_compat_l a b c).
+  rewrite !Z.gt_lt_iff. apply Z.add_lt_mono_r.
 Qed.
 
-Lemma Zplus_lt_compat_l : forall n m p:Z, n < m -> p + n < p + m.
+Lemma Zplus_le_compat_l n m p : n <= m -> p + n <= p + m.
 Proof.
-  unfold Zlt in |- *; intros n m p; rewrite Zcompare_plus_compat;
-    trivial with arith.
+  apply Z.add_le_mono_l.
 Qed.
 
-Lemma Zplus_lt_compat_r : forall n m p:Z, n < m -> n + p < m + p.
+Lemma Zplus_le_compat_r n m p : n <= m -> n + p <= m + p.
 Proof.
-  intros n m p H; rewrite (Zplus_comm n p); rewrite (Zplus_comm m p);
-    apply Zplus_lt_compat_l; trivial.
+  apply Z.add_le_mono_r.
 Qed.
 
-Lemma Zplus_lt_le_compat : forall n m p q:Z, n < m -> p <= q -> n + p < m + q.
+Lemma Zplus_lt_compat_l n m p : n < m -> p + n < p + m.
 Proof.
-  intros a b c d H0 H1.
-  apply Zlt_le_trans with (b + c).
-  apply Zplus_lt_compat_r; trivial.
-  apply Zplus_le_compat_l; trivial.
+  apply Z.add_lt_mono_l.
 Qed.
 
-Lemma Zplus_le_lt_compat : forall n m p q:Z, n <= m -> p < q -> n + p < m + q.
+Lemma Zplus_lt_compat_r n m p : n < m -> n + p < m + p.
 Proof.
-  intros a b c d H0 H1.
-  apply Zle_lt_trans with (b + c).
-  apply Zplus_le_compat_r; trivial.
-  apply Zplus_lt_compat_l; trivial.
+  apply Z.add_lt_mono_r.
 Qed.
 
-Lemma Zplus_le_compat : forall n m p q:Z, n <= m -> p <= q -> n + p <= m + q.
-Proof.
-  intros n m p q; intros H1 H2; apply Zle_trans with (m := n + q);
-    [ apply Zplus_le_compat_l; assumption
-      | apply Zplus_le_compat_r; assumption ].
-Qed.
-
-
-Lemma Zplus_lt_compat : forall n m p q:Z, n < m -> p < q -> n + p < m + q.
-  intros; apply Zplus_le_lt_compat. apply Zlt_le_weak; assumption. assumption.
-Qed.
-
-
 (** Compatibility of addition wrt to being positive *)
 
-Lemma Zplus_le_0_compat : forall n m:Z, 0 <= n -> 0 <= m -> 0 <= n + m.
-Proof.
-  intros x y H1 H2; rewrite <- (Zplus_0_l 0); apply Zplus_le_compat; assumption.
-Qed.
+Notation Zplus_le_0_compat := Z.add_nonneg_nonneg (only parsing).
 
 (** Simplification of addition wrt to order *)
 
-Lemma Zplus_gt_reg_l : forall n m p:Z, p + n > p + m -> n > m.
+Lemma Zplus_le_reg_l n m p : p + n <= p + m -> n <= m.
 Proof.
-  unfold Zgt in |- *; intros n m p H; rewrite <- (Zcompare_plus_compat n m p);
-    assumption.
+ apply Z.add_le_mono_l.
 Qed.
 
-Lemma Zplus_gt_reg_r : forall n m p:Z, n + p > m + p -> n > m.
+Lemma Zplus_le_reg_r n m p : n + p <= m + p -> n <= m.
 Proof.
-  intros n m p H; apply Zplus_gt_reg_l with p.
-  rewrite (Zplus_comm p n); rewrite (Zplus_comm p m); trivial.
+ apply Z.add_le_mono_r.
 Qed.
 
-Lemma Zplus_le_reg_l : forall n m p:Z, p + n <= p + m -> n <= m.
+Lemma Zplus_lt_reg_l n m p : p + n < p + m -> n < m.
 Proof.
-  intros n m p; unfold Zle, not in |- *; intros H1 H2; apply H1;
-    rewrite (Zcompare_plus_compat n m p); assumption.
+ apply Z.add_lt_mono_l.
 Qed.
 
-Lemma Zplus_le_reg_r : forall n m p:Z, n + p <= m + p -> n <= m.
+Lemma Zplus_lt_reg_r n m p : n + p < m + p -> n < m.
 Proof.
-  intros n m p H; apply Zplus_le_reg_l with p.
-  rewrite (Zplus_comm p n); rewrite (Zplus_comm p m); trivial.
+ apply Z.add_lt_mono_r.
 Qed.
 
-Lemma Zplus_lt_reg_l : forall n m p:Z, p + n < p + m -> n < m.
+Lemma Zplus_gt_reg_l n m p : p + n > p + m -> n > m.
 Proof.
-  unfold Zlt in |- *; intros n m p; rewrite Zcompare_plus_compat;
-    trivial with arith.
+ rewrite !Z.gt_lt_iff. apply Z.add_lt_mono_l.
 Qed.
 
-Lemma Zplus_lt_reg_r : forall n m p:Z, n + p < m + p -> n < m.
+Lemma Zplus_gt_reg_r n m p : n + p > m + p -> n > m.
 Proof.
-  intros n m p H; apply Zplus_lt_reg_l with p.
-  rewrite (Zplus_comm p n); rewrite (Zplus_comm p m); trivial.
+ rewrite !Z.gt_lt_iff. apply Z.add_lt_mono_r.
 Qed.
 
 (** ** Multiplication *)
 (** Compatibility of multiplication by a positive wrt to order *)
 
-Lemma Zmult_le_compat_r : forall n m p:Z, n <= m -> 0 <= p -> n * p <= m * p.
+Lemma Zmult_le_compat_r n m p : n <= m -> 0 <= p -> n * p <= m * p.
 Proof.
-  intros a b c H H0; destruct c.
-  do 2 rewrite Zmult_0_r; assumption.
-  rewrite (Zmult_comm a); rewrite (Zmult_comm b).
-  unfold Zle in |- *; rewrite Zcompare_mult_compat; assumption.
-  unfold Zle in H0; contradiction H0; reflexivity.
+ intros. now apply Z.mul_le_mono_nonneg_r.
 Qed.
 
-Lemma Zmult_le_compat_l : forall n m p:Z, n <= m -> 0 <= p -> p * n <= p * m.
+Lemma Zmult_le_compat_l n m p : n <= m -> 0 <= p -> p * n <= p * m.
 Proof.
-  intros a b c H1 H2; rewrite (Zmult_comm c a); rewrite (Zmult_comm c b).
-  apply Zmult_le_compat_r; trivial.
+ intros. now apply Z.mul_le_mono_nonneg_l.
 Qed.
 
-Lemma Zmult_lt_compat_r : forall n m p:Z, 0 < p -> n < m -> n * p < m * p.
+Lemma Zmult_lt_compat_r n m p : 0 < p -> n < m -> n * p < m * p.
 Proof.
-  intros x y z H H0; destruct z.
-  contradiction (Zlt_irrefl 0).
-  rewrite (Zmult_comm x); rewrite (Zmult_comm y).
-  unfold Zlt in |- *; rewrite Zcompare_mult_compat; assumption.
-  discriminate H.
+ apply Z.mul_lt_mono_pos_r.
 Qed.
 
-Lemma Zmult_gt_compat_r : forall n m p:Z, p > 0 -> n > m -> n * p > m * p.
+Lemma Zmult_gt_compat_r n m p : p > 0 -> n > m -> n * p > m * p.
 Proof.
-  intros x y z; intros; apply Zlt_gt; apply Zmult_lt_compat_r; apply Zgt_lt;
-    assumption.
+ rewrite !Z.gt_lt_iff. apply Z.mul_lt_mono_pos_r.
 Qed.
 
-Lemma Zmult_gt_0_lt_compat_r :
-  forall n m p:Z, p > 0 -> n < m -> n * p < m * p.
+Lemma Zmult_gt_0_lt_compat_r n m p : p > 0 -> n < m -> n * p < m * p.
 Proof.
-  intros x y z; intros; apply Zmult_lt_compat_r;
-    [ apply Zgt_lt; assumption | assumption ].
+ rewrite Z.gt_lt_iff. apply Z.mul_lt_mono_pos_r.
 Qed.
 
-Lemma Zmult_gt_0_le_compat_r :
-  forall n m p:Z, p > 0 -> n <= m -> n * p <= m * p.
+Lemma Zmult_gt_0_le_compat_r n m p : p > 0 -> n <= m -> n * p <= m * p.
 Proof.
-  intros x y z Hz Hxy.
-  elim (Zle_lt_or_eq x y Hxy).
-  intros; apply Zlt_le_weak.
-  apply Zmult_gt_0_lt_compat_r; trivial.
-  intros; apply Zeq_le.
-  rewrite H; trivial.
+ rewrite Z.gt_lt_iff. apply Z.mul_le_mono_pos_r.
 Qed.
 
-Lemma Zmult_lt_0_le_compat_r :
-  forall n m p:Z, 0 < p -> n <= m -> n * p <= m * p.
+Lemma Zmult_lt_0_le_compat_r n m p : 0 < p -> n <= m -> n * p <= m * p.
 Proof.
-  intros x y z; intros; apply Zmult_gt_0_le_compat_r; try apply Zlt_gt;
-    assumption.
+ apply Z.mul_le_mono_pos_r.
 Qed.
 
-Lemma Zmult_gt_0_lt_compat_l :
-  forall n m p:Z, p > 0 -> n < m -> p * n < p * m.
+Lemma Zmult_gt_0_lt_compat_l n m p : p > 0 -> n < m -> p * n < p * m.
 Proof.
-  intros x y z; intros.
-  rewrite (Zmult_comm z x); rewrite (Zmult_comm z y);
-    apply Zmult_gt_0_lt_compat_r; assumption.
+ rewrite Z.gt_lt_iff. apply Z.mul_lt_mono_pos_l.
 Qed.
 
-Lemma Zmult_lt_compat_l : forall n m p:Z, 0 < p -> n < m -> p * n < p * m.
+Lemma Zmult_lt_compat_l n m p : 0 < p -> n < m -> p * n < p * m.
 Proof.
-  intros x y z; intros.
-  rewrite (Zmult_comm z x); rewrite (Zmult_comm z y);
-    apply Zmult_gt_0_lt_compat_r; try apply Zlt_gt; assumption.
+ apply Z.mul_lt_mono_pos_l.
 Qed.
 
-Lemma Zmult_gt_compat_l : forall n m p:Z, p > 0 -> n > m -> p * n > p * m.
+Lemma Zmult_gt_compat_l n m p : p > 0 -> n > m -> p * n > p * m.
 Proof.
-  intros x y z; intros; rewrite (Zmult_comm z x); rewrite (Zmult_comm z y);
-    apply Zmult_gt_compat_r; assumption.
+ rewrite !Z.gt_lt_iff. apply Z.mul_lt_mono_pos_l.
 Qed.
 
-Lemma Zmult_ge_compat_r : forall n m p:Z, n >= m -> p >= 0 -> n * p >= m * p.
+Lemma Zmult_ge_compat_r n m p : n >= m -> p >= 0 -> n * p >= m * p.
 Proof.
-  intros a b c H1 H2; apply Zle_ge.
-  apply Zmult_le_compat_r; apply Zge_le; trivial.
+ rewrite !Z.ge_le_iff. intros. now apply Z.mul_le_mono_nonneg_r.
 Qed.
 
-Lemma Zmult_ge_compat_l : forall n m p:Z, n >= m -> p >= 0 -> p * n >= p * m.
+Lemma Zmult_ge_compat_l n m p : n >= m -> p >= 0 -> p * n >= p * m.
 Proof.
-  intros a b c H1 H2; apply Zle_ge.
-  apply Zmult_le_compat_l; apply Zge_le; trivial.
+ rewrite !Z.ge_le_iff. intros. now apply Z.mul_le_mono_nonneg_l.
 Qed.
 
-Lemma Zmult_ge_compat :
-  forall n m p q:Z, n >= p -> m >= q -> p >= 0 -> q >= 0 -> n * m >= p * q.
+Lemma Zmult_ge_compat n m p q :
+  n >= p -> m >= q -> p >= 0 -> q >= 0 -> n * m >= p * q.
 Proof.
-  intros a b c d H0 H1 H2 H3.
-  apply Zge_trans with (a * d).
-  apply Zmult_ge_compat_l; trivial.
-  apply Zge_trans with c; trivial.
-  apply Zmult_ge_compat_r; trivial.
+ rewrite !Z.ge_le_iff. intros. now apply Z.mul_le_mono_nonneg.
 Qed.
 
-Lemma Zmult_le_compat :
-  forall n m p q:Z, n <= p -> m <= q -> 0 <= n -> 0 <= m -> n * m <= p * q.
+Lemma Zmult_le_compat n m p q :
+  n <= p -> m <= q -> 0 <= n -> 0 <= m -> n * m <= p * q.
 Proof.
-  intros a b c d H0 H1 H2 H3.
-  apply Zle_trans with (c * b).
-  apply Zmult_le_compat_r; assumption.
-  apply Zmult_le_compat_l.
-  assumption.
-  apply Zle_trans with a; assumption.
+ intros. now apply Z.mul_le_mono_nonneg.
 Qed.
 
 (** Simplification of multiplication by a positive wrt to being positive *)
 
-Lemma Zmult_gt_0_lt_reg_r : forall n m p:Z, p > 0 -> n * p < m * p -> n < m.
+Lemma Zmult_gt_0_lt_reg_r n m p : p > 0 -> n * p < m * p -> n < m.
 Proof.
-  intros x y z; intros; destruct z.
-  contradiction (Zgt_irrefl 0).
-  rewrite (Zmult_comm x) in H0; rewrite (Zmult_comm y) in H0.
-  unfold Zlt in H0; rewrite Zcompare_mult_compat in H0; assumption.
-  discriminate H.
+ rewrite Z.gt_lt_iff. apply Z.mul_lt_mono_pos_r.
 Qed.
 
-Lemma Zmult_lt_reg_r : forall n m p:Z, 0 < p -> n * p < m * p -> n < m.
+Lemma Zmult_lt_reg_r n m p : 0 < p -> n * p < m * p -> n < m.
 Proof.
-  intros a b c H0 H1.
-  apply Zmult_gt_0_lt_reg_r with c; try apply Zlt_gt; assumption.
+ apply Z.mul_lt_mono_pos_r.
 Qed.
 
-Lemma Zmult_le_reg_r : forall n m p:Z, p > 0 -> n * p <= m * p -> n <= m.
+Lemma Zmult_le_reg_r n m p : p > 0 -> n * p <= m * p -> n <= m.
 Proof.
-  intros x y z Hz Hxy.
-  elim (Zle_lt_or_eq (x * z) (y * z) Hxy).
-  intros; apply Zlt_le_weak.
-  apply Zmult_gt_0_lt_reg_r with z; trivial.
-  intros; apply Zeq_le.
-  apply Zmult_reg_r with z.
-  intro. rewrite H0 in Hz. contradiction (Zgt_irrefl 0).
-  assumption.
+ rewrite Z.gt_lt_iff. apply Z.mul_le_mono_pos_r.
 Qed.
 
-Lemma Zmult_lt_0_le_reg_r : forall n m p:Z, 0 < p -> n * p <= m * p -> n <= m.
+Lemma Zmult_lt_0_le_reg_r n m p : 0 < p -> n * p <= m * p -> n <= m.
 Proof.
-  intros x y z; intros; apply Zmult_le_reg_r with z.
-  try apply Zlt_gt; assumption.
-  assumption.
+ apply Z.mul_le_mono_pos_r.
 Qed.
 
-
-Lemma Zmult_ge_reg_r : forall n m p:Z, p > 0 -> n * p >= m * p -> n >= m.
+Lemma Zmult_ge_reg_r n m p : p > 0 -> n * p >= m * p -> n >= m.
 Proof.
-  intros a b c H1 H2; apply Zle_ge; apply Zmult_le_reg_r with c; trivial.
-  apply Zge_le; trivial.
+ rewrite Z.gt_lt_iff, !Z.ge_le_iff. apply Z.mul_le_mono_pos_r.
 Qed.
 
-Lemma Zmult_gt_reg_r : forall n m p:Z, p > 0 -> n * p > m * p -> n > m.
+Lemma Zmult_gt_reg_r n m p : p > 0 -> n * p > m * p -> n > m.
 Proof.
-  intros a b c H1 H2; apply Zlt_gt; apply Zmult_gt_0_lt_reg_r with c; trivial.
-  apply Zgt_lt; trivial.
+ rewrite !Z.gt_lt_iff. apply Z.mul_lt_mono_pos_r.
 Qed.
 
-
-(** Compatibility of multiplication by a positive wrt to being positive *)
-
-Lemma Zmult_le_0_compat : forall n m:Z, 0 <= n -> 0 <= m -> 0 <= n * m.
+Lemma Zmult_lt_compat n m p q :
+  0 <= n < p -> 0 <= m < q -> n * m < p * q.
 Proof.
-  intros x y; case x.
-  intros; rewrite Zmult_0_l; trivial.
-  intros p H1; unfold Zle in |- *.
-  pattern 0 at 2 in |- *; rewrite <- (Zmult_0_r (Zpos p)).
-  rewrite Zcompare_mult_compat; trivial.
-  intros p H1 H2; absurd (0 > Zneg p); trivial.
-  unfold Zgt in |- *; simpl in |- *; auto with zarith.
+ intros (Hn,Hnp) (Hm,Hmq). now apply Z.mul_lt_mono_nonneg.
 Qed.
 
-Lemma Zmult_gt_0_compat : forall n m:Z, n > 0 -> m > 0 -> n * m > 0.
+Lemma Zmult_lt_compat2 n m p q :
+  0 < n <= p -> 0 < m < q -> n * m < p * q.
 Proof.
-  intros x y; case x.
-  intros H; discriminate H.
-  intros p H1; unfold Zgt in |- *; pattern 0 at 2 in |- *;
-    rewrite <- (Zmult_0_r (Zpos p)).
-  rewrite Zcompare_mult_compat; trivial.
-  intros p H; discriminate H.
+  intros (Hn, Hnp) (Hm,Hmq).
+  apply Z.le_lt_trans with (p * m).
+   apply Z.mul_le_mono_pos_r; trivial.
+   apply Z.mul_lt_mono_pos_l; Z.order.
 Qed.
 
-Lemma Zmult_lt_0_compat : forall n m:Z, 0 < n -> 0 < m -> 0 < n * m.
+(** Compatibility of multiplication by a positive wrt to being positive *)
+
+Notation Zmult_le_0_compat := Z.mul_nonneg_nonneg (only parsing).
+Notation Zmult_lt_0_compat := Z.mul_pos_pos (only parsing).
+Notation Zmult_lt_O_compat := Z.mul_pos_pos (only parsing).
+
+Lemma Zmult_gt_0_compat n m : n > 0 -> m > 0 -> n * m > 0.
 Proof.
-  intros a b apos bpos.
-  apply Zgt_lt.
-  apply Zmult_gt_0_compat; try apply Zlt_gt; assumption.
+ rewrite !Z.gt_lt_iff. apply Z.mul_pos_pos.
 Qed.
 
-(** For compatibility *)
-Notation Zmult_lt_O_compat := Zmult_lt_0_compat (only parsing).
-
-Lemma Zmult_gt_0_le_0_compat : forall n m:Z, n > 0 -> 0 <= m -> 0 <= m * n.
+(* TODO: to remove ? *)
+Lemma Zmult_gt_0_le_0_compat n m : n > 0 -> 0 <= m -> 0 <= m * n.
 Proof.
-  intros x y H1 H2; apply Zmult_le_0_compat; trivial.
-  apply Zlt_le_weak; apply Zgt_lt; trivial.
+ rewrite Z.gt_lt_iff. intros. apply Z.mul_nonneg_nonneg. trivial.
+  now apply Z.lt_le_incl.
 Qed.
 
 (** Simplification of multiplication by a positive wrt to being positive *)
 
-Lemma Zmult_le_0_reg_r : forall n m:Z, n > 0 -> 0 <= m * n -> 0 <= m.
+Lemma Zmult_le_0_reg_r n m : n > 0 -> 0 <= m * n -> 0 <= m.
 Proof.
-  intros x y; case x;
-    [ simpl in |- *; unfold Zgt in |- *; simpl in |- *; intros H; discriminate H
-      | intros p H1; unfold Zle in |- *; rewrite Zmult_comm;
-	pattern 0 at 1 in |- *; rewrite <- (Zmult_0_r (Zpos p));
-	  rewrite Zcompare_mult_compat; auto with arith
-      | intros p; unfold Zgt in |- *; simpl in |- *; intros H; discriminate H ].
+ rewrite Z.gt_lt_iff. intros Hn Hmn.
+ destruct (Z.le_0_mul _ _ Hmn) as [[Hm _]|[_ Hn']]; Z.order.
 Qed.
 
-Lemma Zmult_gt_0_lt_0_reg_r : forall n m:Z, n > 0 -> 0 < m * n -> 0 < m.
+(* TODO move to numbers ? *)
+Lemma Zmult_lt_0_reg_r n m : 0 < n -> 0 < m * n -> 0 < m.
 Proof.
-  intros x y; case x;
-    [ simpl in |- *; unfold Zgt in |- *; simpl in |- *; intros H; discriminate H
-      | intros p H1; unfold Zlt in |- *; rewrite Zmult_comm;
-	pattern 0 at 1 in |- *; rewrite <- (Zmult_0_r (Zpos p));
-	  rewrite Zcompare_mult_compat; auto with arith
-      | intros p; unfold Zgt in |- *; simpl in |- *; intros H; discriminate H ].
+ intros Hn Hmn.
+ rewrite Z.lt_0_mul in Hmn. destruct Hmn as [[Hm _]|[Hn' _]]; Z.order.
 Qed.
 
-Lemma Zmult_lt_0_reg_r : forall n m:Z, 0 < n -> 0 < m * n -> 0 < m.
+Lemma Zmult_gt_0_lt_0_reg_r n m : n > 0 -> 0 < m * n -> 0 < m.
 Proof.
-  intros x y; intros; eapply Zmult_gt_0_lt_0_reg_r with x; try apply Zlt_gt;
-    assumption.
+ rewrite Z.gt_lt_iff. apply Zmult_lt_0_reg_r.
 Qed.
 
-Lemma Zmult_gt_0_reg_l : forall n m:Z, n > 0 -> n * m > 0 -> m > 0.
+Lemma Zmult_gt_0_reg_l n m : n > 0 -> n * m > 0 -> m > 0.
 Proof.
-  intros x y; case x.
-  intros H; discriminate H.
-  intros p H1; unfold Zgt in |- *.
-  pattern 0 at 1 in |- *; rewrite <- (Zmult_0_r (Zpos p)).
-  rewrite Zcompare_mult_compat; trivial.
-  intros p H; discriminate H.
+ rewrite !Z.gt_lt_iff. rewrite Z.mul_comm. apply Zmult_lt_0_reg_r.
 Qed.
 
 (** ** Square *)
 (** Simplification of square wrt order *)
 
-Lemma Zgt_square_simpl :
-  forall n m:Z, n >= 0 -> n * n > m * m -> n > m.
+Lemma Zlt_square_simpl n m : 0 <= n -> m * m < n * n -> m < n.
 Proof.
-  intros n m H0 H1.
-  case (dec_Zlt m n).
-  intro; apply Zlt_gt; trivial.
-  intros H2; cut (m >= n).
-  intros H.
-  elim Zgt_not_le with (1 := H1).
-  apply Zge_le.
-  apply Zmult_ge_compat; auto.
-  apply Znot_lt_ge; trivial.
+ apply Z.square_lt_simpl_nonneg.
 Qed.
 
-Lemma Zlt_square_simpl :
-  forall n m:Z, 0 <= n -> m * m < n * n -> m < n.
+Lemma Zgt_square_simpl n m : n >= 0 -> n * n > m * m -> n > m.
 Proof.
-  intros x y H0 H1.
-  apply Zgt_lt.
-  apply Zgt_square_simpl; try apply Zle_ge; try apply Zlt_gt; assumption.
+ rewrite !Z.gt_lt_iff, Z.ge_le_iff. apply Z.square_lt_simpl_nonneg.
 Qed.
 
 (** * Equivalence between inequalities *)
 
-Lemma Zle_plus_swap : forall n m p:Z, n + p <= m <-> n <= m - p.
-Proof.
-  intros x y z; intros. split. intro. rewrite <- (Zplus_0_r x). rewrite <- (Zplus_opp_r z).
-  rewrite Zplus_assoc. exact (Zplus_le_compat_r _ _ _ H).
-  intro. rewrite <- (Zplus_0_r y). rewrite <- (Zplus_opp_l z). rewrite Zplus_assoc.
-  apply Zplus_le_compat_r. assumption.
-Qed.
-
-Lemma Zlt_plus_swap : forall n m p:Z, n + p < m <-> n < m - p.
-Proof.
-  intros x y z; intros. split. intro. unfold Zminus in |- *. rewrite Zplus_comm. rewrite <- (Zplus_0_l x).
-  rewrite <- (Zplus_opp_l z). rewrite Zplus_assoc_reverse. apply Zplus_lt_compat_l. rewrite Zplus_comm.
-  assumption.
-  intro. rewrite Zplus_comm. rewrite <- (Zplus_0_l y). rewrite <- (Zplus_opp_r z).
-  rewrite Zplus_assoc_reverse. apply Zplus_lt_compat_l. rewrite Zplus_comm. assumption.
-Qed.
-
-Lemma Zeq_plus_swap : forall n m p:Z, n + p = m <-> n = m - p.
-Proof.
-  intros x y z; intros. split. intro. apply Zplus_minus_eq. symmetry  in |- *. rewrite Zplus_comm.
-  assumption.
-  intro. rewrite H. unfold Zminus in |- *. rewrite Zplus_assoc_reverse.
-  rewrite Zplus_opp_l. apply Zplus_0_r.
-Qed.
-
-Lemma Zlt_minus_simpl_swap : forall n m:Z, 0 < m -> n - m < n.
-Proof.
-  intros n m H; apply Zplus_lt_reg_l with (p := m); rewrite Zplus_minus;
-    pattern n at 1 in |- *; rewrite <- (Zplus_0_r n);
-      rewrite (Zplus_comm m n); apply Zplus_lt_compat_l;
-	assumption.
-Qed.
-
-Lemma Zlt_0_minus_lt : forall n m:Z, 0 < n - m -> m < n.
-Proof.
-  intros n m H; apply Zplus_lt_reg_l with (p := - m); rewrite Zplus_opp_l;
-    rewrite Zplus_comm; exact H.
-Qed.
+Notation Zle_plus_swap := Z.le_add_le_sub_r (only parsing).
+Notation Zlt_plus_swap := Z.lt_add_lt_sub_r (only parsing).
+Notation Zlt_minus_simpl_swap := Z.lt_sub_pos (only parsing).
 
-Lemma Zle_0_minus_le : forall n m:Z, 0 <= n - m -> m <= n.
+Lemma Zeq_plus_swap n m p : n + p = m <-> n = m - p.
 Proof.
-  intros n m H; apply Zplus_le_reg_l with (p := - m); rewrite Zplus_opp_l;
-    rewrite Zplus_comm; exact H.
+ apply Z.add_move_r.
 Qed.
 
-Lemma Zle_minus_le_0 : forall n m:Z, m <= n -> 0 <= n - m.
+Lemma Zlt_0_minus_lt n m : 0 < n - m -> m < n.
 Proof.
-  intros n m H; unfold Zminus; apply Zplus_le_reg_r with (p := m);
-    rewrite <- Zplus_assoc; rewrite Zplus_opp_l; rewrite Zplus_0_r; exact H.
+ apply Z.lt_0_sub.
 Qed.
 
-Lemma Zmult_lt_compat:
-  forall n m p q : Z, 0 <= n < p -> 0 <= m < q -> n * m < p * q.
+Lemma Zle_0_minus_le n m : 0 <= n - m -> m <= n.
 Proof.
-  intros n m p q (H1, H2) (H3,H4).
-  assert (0<p) by (apply Zle_lt_trans with n; auto).
-  assert (0<q) by (apply Zle_lt_trans with m; auto).
-  case Zle_lt_or_eq with (1 := H1); intros H5; auto with zarith.
-  case Zle_lt_or_eq with (1 := H3); intros H6; auto with zarith.
-  apply Zlt_trans with (n * q).
-  apply Zmult_lt_compat_l; auto.
-  apply Zmult_lt_compat_r; auto with zarith.
-  rewrite <- H6; rewrite Zmult_0_r; apply Zmult_lt_0_compat; auto with zarith.
-  rewrite <- H5; simpl; apply Zmult_lt_0_compat; auto with zarith.
+ apply Z.le_0_sub.
 Qed.
 
-Lemma Zmult_lt_compat2:
-  forall n m p q : Z, 0 < n <= p -> 0 < m < q -> n * m < p * q.
+Lemma Zle_minus_le_0 n m : m <= n -> 0 <= n - m.
 Proof.
-  intros n m p q (H1, H2) (H3, H4).
-  apply Zle_lt_trans with (p * m).
-  apply Zmult_le_compat_r; auto.
-  apply Zlt_le_weak; auto.
-  apply Zmult_lt_compat_l; auto.
-  apply Zlt_le_trans with n; auto.
+ apply Z.le_0_sub.
 Qed.
 
 (** For compatibility *)