From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 theories/Arith/Lt.v | 39 +++++++++++++++++++++++----------------
 1 file changed, 23 insertions(+), 16 deletions(-)

(limited to 'theories/Arith/Lt.v')

diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index bfc2b91a..0c7515c6 100644
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (** Strict order on natural numbers.
@@ -23,7 +25,7 @@ Local Open Scope nat_scope.
 
 (** * Irreflexivity *)
 
-Notation lt_irrefl := Nat.lt_irrefl (compat "8.4"). (* ~ x < x *)
+Notation lt_irrefl := Nat.lt_irrefl (only parsing). (* ~ x < x *)
 
 Hint Resolve lt_irrefl: arith.
 
@@ -62,12 +64,12 @@ Hint Immediate le_not_lt lt_not_le: arith.
 
 (** * Asymmetry *)
 
-Notation lt_asym := Nat.lt_asymm (compat "8.4"). (* n<m -> ~m<n *)
+Notation lt_asym := Nat.lt_asymm (only parsing). (* n<m -> ~m<n *)
 
 (** * Order and 0 *)
 
-Notation lt_0_Sn := Nat.lt_0_succ (compat "8.4"). (* 0 < S n *)
-Notation lt_n_0 := Nat.nlt_0_r (compat "8.4"). (* ~ n < 0 *)
+Notation lt_0_Sn := Nat.lt_0_succ (only parsing). (* 0 < S n *)
+Notation lt_n_0 := Nat.nlt_0_r (only parsing). (* ~ n < 0 *)
 
 Theorem neq_0_lt n : 0 <> n -> 0 < n.
 Proof.
@@ -84,8 +86,8 @@ Hint Immediate neq_0_lt lt_0_neq: arith.
 
 (** * Order and successor *)
 
-Notation lt_n_Sn := Nat.lt_succ_diag_r (compat "8.4"). (* n < S n *)
-Notation lt_S := Nat.lt_lt_succ_r (compat "8.4"). (* n < m -> n < S m *)
+Notation lt_n_Sn := Nat.lt_succ_diag_r (only parsing). (* n < S n *)
+Notation lt_S := Nat.lt_lt_succ_r (only parsing). (* n < m -> n < S m *)
 
 Theorem lt_n_S n m : n < m -> S n < S m.
 Proof.
@@ -107,6 +109,11 @@ Proof.
  intros. symmetry. now apply Nat.lt_succ_pred with m.
 Qed.
 
+Lemma S_pred_pos n: O < n -> n = S (pred n).
+Proof.
+ apply S_pred.
+Qed.
+
 Lemma lt_pred n m : S n < m -> n < pred m.
 Proof.
  apply Nat.lt_succ_lt_pred.
@@ -122,28 +129,28 @@ Hint Resolve lt_pred_n_n: arith.
 
 (** * Transitivity properties *)
 
-Notation lt_trans := Nat.lt_trans (compat "8.4").
-Notation lt_le_trans := Nat.lt_le_trans (compat "8.4").
-Notation le_lt_trans := Nat.le_lt_trans (compat "8.4").
+Notation lt_trans := Nat.lt_trans (only parsing).
+Notation lt_le_trans := Nat.lt_le_trans (only parsing).
+Notation le_lt_trans := Nat.le_lt_trans (only parsing).
 
 Hint Resolve lt_trans lt_le_trans le_lt_trans: arith.
 
 (** * Large = strict or equal *)
 
-Notation le_lt_or_eq_iff := Nat.lt_eq_cases (compat "8.4").
+Notation le_lt_or_eq_iff := Nat.lt_eq_cases (only parsing).
 
 Theorem le_lt_or_eq n m : n <= m -> n < m \/ n = m.
 Proof.
  apply Nat.lt_eq_cases.
 Qed.
 
-Notation lt_le_weak := Nat.lt_le_incl (compat "8.4").
+Notation lt_le_weak := Nat.lt_le_incl (only parsing).
 
 Hint Immediate lt_le_weak: arith.
 
 (** * Dichotomy *)
 
-Notation le_or_lt := Nat.le_gt_cases (compat "8.4"). (* n <= m \/ m < n *)
+Notation le_or_lt := Nat.le_gt_cases (only parsing). (* n <= m \/ m < n *)
 
 Theorem nat_total_order n m : n <> m -> n < m \/ m < n.
 Proof.
-- 
cgit v1.2.3