diff options
Diffstat (limited to 'theories/Arith/Le.v')
| -rw-r--r-- | theories/Arith/Le.v | 28 |
1 files changed, 15 insertions, 13 deletions
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v index 0fbcec57..69626cc1 100644 --- a/theories/Arith/Le.v +++ b/theories/Arith/Le.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) *) (************************************************************************) (** Order on natural numbers. @@ -26,17 +28,17 @@ Local Open Scope nat_scope. (** * [le] is an order on [nat] *) -Notation le_refl := Nat.le_refl (compat "8.4"). -Notation le_trans := Nat.le_trans (compat "8.4"). -Notation le_antisym := Nat.le_antisymm (compat "8.4"). +Notation le_refl := Nat.le_refl (only parsing). +Notation le_trans := Nat.le_trans (only parsing). +Notation le_antisym := Nat.le_antisymm (only parsing). Hint Resolve le_trans: arith. Hint Immediate le_antisym: arith. (** * Properties of [le] w.r.t 0 *) -Notation le_0_n := Nat.le_0_l (compat "8.4"). (* 0 <= n *) -Notation le_Sn_0 := Nat.nle_succ_0 (compat "8.4"). (* ~ S n <= 0 *) +Notation le_0_n := Nat.le_0_l (only parsing). (* 0 <= n *) +Notation le_Sn_0 := Nat.nle_succ_0 (only parsing). (* ~ S n <= 0 *) Lemma le_n_0_eq n : n <= 0 -> 0 = n. Proof. @@ -53,8 +55,8 @@ Proof Peano.le_n_S. Theorem le_S_n : forall n m, S n <= S m -> n <= m. Proof Peano.le_S_n. -Notation le_n_Sn := Nat.le_succ_diag_r (compat "8.4"). (* n <= S n *) -Notation le_Sn_n := Nat.nle_succ_diag_l (compat "8.4"). (* ~ S n <= n *) +Notation le_n_Sn := Nat.le_succ_diag_r (only parsing). (* n <= S n *) +Notation le_Sn_n := Nat.nle_succ_diag_l (only parsing). (* ~ S n <= n *) Theorem le_Sn_le : forall n m, S n <= m -> n <= m. Proof Nat.lt_le_incl. @@ -65,8 +67,8 @@ Hint Immediate le_n_0_eq le_Sn_le le_S_n : arith. (** * Properties of [le] w.r.t predecessor *) -Notation le_pred_n := Nat.le_pred_l (compat "8.4"). (* pred n <= n *) -Notation le_pred := Nat.pred_le_mono (compat "8.4"). (* n<=m -> pred n <= pred m *) +Notation le_pred_n := Nat.le_pred_l (only parsing). (* pred n <= n *) +Notation le_pred := Nat.pred_le_mono (only parsing). (* n<=m -> pred n <= pred m *) Hint Resolve le_pred_n: arith. |