From e0d682ec25282a348d35c5b169abafec48555690 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Mon, 20 Aug 2012 18:27:01 +0200
Subject: Imported Upstream version 8.4dfsg

---
 theories/ZArith/Zorder.v | 100 ++++++++++++++++++++++++-----------------------
 1 file changed, 51 insertions(+), 49 deletions(-)

(limited to 'theories/ZArith/Zorder.v')

diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index a8cd69bb..b1d1f8b5 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -38,9 +38,9 @@ Qed.
 (**********************************************************************)
 (** * Decidability of equality and order on Z *)
 
-Notation dec_eq := Z.eq_decidable (only parsing).
-Notation dec_Zle := Z.le_decidable (only parsing).
-Notation dec_Zlt := Z.lt_decidable (only parsing).
+Notation dec_eq := Z.eq_decidable (compat "8.3").
+Notation dec_Zle := Z.le_decidable (compat "8.3").
+Notation dec_Zlt := Z.lt_decidable (compat "8.3").
 
 Theorem dec_Zne n m : decidable (Zne n m).
 Proof.
@@ -64,12 +64,12 @@ Qed.
 
 (** * Relating strict and large orders *)
 
-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).
+Notation Zgt_lt := Z.gt_lt (compat "8.3").
+Notation Zlt_gt := Z.lt_gt (compat "8.3").
+Notation Zge_le := Z.ge_le (compat "8.3").
+Notation Zle_ge := Z.le_ge (compat "8.3").
+Notation Zgt_iff_lt := Z.gt_lt_iff (compat "8.3").
+Notation Zge_iff_le := Z.ge_le_iff (compat "8.3").
 
 Lemma Zle_not_lt n m : n <= m -> ~ m < n.
 Proof.
@@ -121,18 +121,18 @@ Qed.
 
 (** Reflexivity *)
 
-Notation Zle_refl := Z.le_refl (only parsing).
-Notation Zeq_le := Z.eq_le_incl (only parsing).
+Notation Zle_refl := Z.le_refl (compat "8.3").
+Notation Zeq_le := Z.eq_le_incl (compat "8.3").
 
 Hint Resolve Z.le_refl: zarith.
 
 (** Antisymmetry *)
 
-Notation Zle_antisym := Z.le_antisymm (only parsing).
+Notation Zle_antisym := Z.le_antisymm (compat "8.3").
 
 (** Asymmetry *)
 
-Notation Zlt_asym := Z.lt_asymm (only parsing).
+Notation Zlt_asym := Z.lt_asymm (compat "8.3").
 
 Lemma Zgt_asym n m : n > m -> ~ m > n.
 Proof.
@@ -141,8 +141,8 @@ Qed.
 
 (** Irreflexivity *)
 
-Notation Zlt_irrefl := Z.lt_irrefl (only parsing).
-Notation Zlt_not_eq := Z.lt_neq (only parsing).
+Notation Zlt_irrefl := Z.lt_irrefl (compat "8.3").
+Notation Zlt_not_eq := Z.lt_neq (compat "8.3").
 
 Lemma Zgt_irrefl n : ~ n > n.
 Proof.
@@ -151,8 +151,8 @@ Qed.
 
 (** Large = strict or equal *)
 
-Notation Zlt_le_weak := Z.lt_le_incl (only parsing).
-Notation Zle_lt_or_eq_iff := Z.lt_eq_cases (only parsing).
+Notation Zlt_le_weak := Z.lt_le_incl (compat "8.3").
+Notation Zle_lt_or_eq_iff := Z.lt_eq_cases (compat "8.3").
 
 Lemma Zle_lt_or_eq n m : n <= m -> n < m \/ n = m.
 Proof.
@@ -161,19 +161,21 @@ Qed.
 
 (** Dichotomy *)
 
-Notation Zle_or_lt := Z.le_gt_cases (only parsing).
+Notation Zle_or_lt := Z.le_gt_cases (compat "8.3").
 
 (** Transitivity of strict orders *)
 
-Notation Zlt_trans := Z.lt_trans (only parsing).
+Notation Zlt_trans := Z.lt_trans (compat "8.3").
 
-Lemma Zgt_trans : forall n m p:Z, n > m -> m > p -> n > p.
-Proof Zcompare_Gt_trans.
+Lemma Zgt_trans n m p : n > m -> m > p -> n > p.
+Proof.
+  Z.swap_greater. intros; now transitivity m.
+Qed.
 
 (** Mixed transitivity *)
 
-Notation Zlt_le_trans := Z.lt_le_trans (only parsing).
-Notation Zle_lt_trans := Z.le_lt_trans (only parsing).
+Notation Zlt_le_trans := Z.lt_le_trans (compat "8.3").
+Notation Zle_lt_trans := Z.le_lt_trans (compat "8.3").
 
 Lemma Zle_gt_trans n m p : m <= n -> m > p -> n > p.
 Proof.
@@ -187,7 +189,7 @@ Qed.
 
 (** Transitivity of large orders *)
 
-Notation Zle_trans := Z.le_trans (only parsing).
+Notation Zle_trans := Z.le_trans (compat "8.3").
 
 Lemma Zge_trans n m p : n >= m -> m >= p -> n >= p.
 Proof.
@@ -238,8 +240,8 @@ Qed.
 
 (** Special base instances of order *)
 
-Notation Zlt_succ := Z.lt_succ_diag_r (only parsing).
-Notation Zlt_pred := Z.lt_pred_l (only parsing).
+Notation Zlt_succ := Z.lt_succ_diag_r (compat "8.3").
+Notation Zlt_pred := Z.lt_pred_l (compat "8.3").
 
 Lemma Zgt_succ n : Z.succ n > n.
 Proof.
@@ -253,8 +255,8 @@ Qed.
 
 (** Relating strict and large order using successor or predecessor *)
 
-Notation Zlt_succ_r := Z.lt_succ_r (only parsing).
-Notation Zle_succ_l := Z.le_succ_l (only parsing).
+Notation Zlt_succ_r := Z.lt_succ_r (compat "8.3").
+Notation Zle_succ_l := Z.le_succ_l (compat "8.3").
 
 Lemma Zgt_le_succ n m : m > n -> Z.succ n <= m.
 Proof.
@@ -293,10 +295,10 @@ Qed.
 
 (** Weakening order *)
 
-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).
+Notation Zle_succ := Z.le_succ_diag_r (compat "8.3").
+Notation Zle_pred := Z.le_pred_l (compat "8.3").
+Notation Zlt_lt_succ := Z.lt_lt_succ_r (compat "8.3").
+Notation Zle_le_succ := Z.le_le_succ_r (compat "8.3").
 
 Lemma Zle_succ_le n m : Z.succ n <= m -> n <= m.
 Proof.
@@ -304,7 +306,7 @@ Proof.
 Qed.
 
 Hint Resolve Z.le_succ_diag_r: zarith.
-Hint Resolve Zle_le_succ: zarith.
+Hint Resolve Z.le_le_succ_r: zarith.
 
 (** Relating order wrt successor and order wrt predecessor *)
 
@@ -332,8 +334,8 @@ Qed.
 
 (** Special cases of ordered integers *)
 
-Notation Zlt_0_1 := Z.lt_0_1 (only parsing).
-Notation Zle_0_1 := Z.le_0_1 (only parsing).
+Notation Zlt_0_1 := Z.lt_0_1 (compat "8.3").
+Notation Zle_0_1 := Z.le_0_1 (compat "8.3").
 
 Lemma Zle_neg_pos : forall p q:positive, Zneg p <= Zpos q.
 Proof.
@@ -345,7 +347,7 @@ Proof.
   easy.
 Qed.
 
-(* weaker but useful (in [Zpower] for instance) *)
+(* weaker but useful (in [Z.pow] for instance) *)
 Lemma Zle_0_pos : forall p:positive, 0 <= Zpos p.
 Proof.
  easy.
@@ -361,7 +363,7 @@ Proof.
   induction n; simpl; intros. apply Z.le_refl. easy.
 Qed.
 
-Hint Immediate Zeq_le: zarith.
+Hint Immediate Z.eq_le_incl: zarith.
 
 (** Derived lemma *)
 
@@ -373,10 +375,10 @@ Qed.
 (** ** Addition *)
 (** Compatibility of addition wrt to order *)
 
-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).
+Notation Zplus_lt_le_compat := Z.add_lt_le_mono (compat "8.3").
+Notation Zplus_le_lt_compat := Z.add_le_lt_mono (compat "8.3").
+Notation Zplus_le_compat := Z.add_le_mono (compat "8.3").
+Notation Zplus_lt_compat := Z.add_lt_mono (compat "8.3").
 
 Lemma Zplus_gt_compat_l n m p : n > m -> p + n > p + m.
 Proof.
@@ -410,7 +412,7 @@ Qed.
 
 (** Compatibility of addition wrt to being positive *)
 
-Notation Zplus_le_0_compat := Z.add_nonneg_nonneg (only parsing).
+Notation Zplus_le_0_compat := Z.add_nonneg_nonneg (compat "8.3").
 
 (** Simplification of addition wrt to order *)
 
@@ -568,9 +570,9 @@ Qed.
 
 (** 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).
+Notation Zmult_le_0_compat := Z.mul_nonneg_nonneg (compat "8.3").
+Notation Zmult_lt_0_compat := Z.mul_pos_pos (compat "8.3").
+Notation Zmult_lt_O_compat := Z.mul_pos_pos (compat "8.3").
 
 Lemma Zmult_gt_0_compat n m : n > 0 -> m > 0 -> n * m > 0.
 Proof.
@@ -622,9 +624,9 @@ Qed.
 
 (** * Equivalence between inequalities *)
 
-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).
+Notation Zle_plus_swap := Z.le_add_le_sub_r (compat "8.3").
+Notation Zlt_plus_swap := Z.lt_add_lt_sub_r (compat "8.3").
+Notation Zlt_minus_simpl_swap := Z.lt_sub_pos (compat "8.3").
 
 Lemma Zeq_plus_swap n m p : n + p = m <-> n = m - p.
 Proof.
-- 
cgit v1.2.3