From 6eb9b908400fd51a4d8996a47b14146eaa69371f Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Fri, 18 Feb 2022 12:58:34 +0100
Subject: [PATCH] Remove unused section

---
 util/nat.v | 32 +++++++++++---------------------
 1 file changed, 11 insertions(+), 21 deletions(-)

diff --git a/util/nat.v b/util/nat.v
index ad39e8a29..36d335e52 100644
--- a/util/nat.v
+++ b/util/nat.v
@@ -115,26 +115,16 @@ Section Interval.
 
 End Interval.
 
-(** In the section, we introduce an additional lemma about relation
-    [<] over natural numbers.  *)
-Section NatOrderLemmas.
+(* [ltn_leq_trans]: Establish that [m < p] if [m < n] and [n <= p], to mirror the
+   lemma [leq_ltn_trans] in [ssrnat].
 
-  (* Mimic the way implicit arguments are used in [ssreflect]. *)
-  Set Implicit Arguments.
-  Unset Strict Implicit.
+   NB: There is a good reason for this lemma to be "missing" in [ssrnat] --
+   since [m < n] is defined as [m.+1 <= n], [ltn_leq_trans] is just
+   [m.+1 <= n -> n <= p -> m.+1 <= p], that is [@leq_trans n m.+1 p].
 
-  (* [ltn_leq_trans]: Establish that [m < p] if [m < n] and [n <= p], to mirror the
-     lemma [leq_ltn_trans] in [ssrnat].
-
-     NB: There is a good reason for this lemma to be "missing" in [ssrnat] --
-     since [m < n] is defined as [m.+1 <= n], [ltn_leq_trans] is just
-     [m.+1 <= n -> n <= p -> m.+1 <= p], that is [@leq_trans n m.+1 p].
-
-     Nonetheless we introduce it here because an additional (even though
-     arguably redundant) lemma doesn't hurt, and for newcomers the apparent
-     absence of the mirror case of [leq_ltn_trans] can be somewhat confusing.  *)
-  #[deprecated(since="0.4",note="Use leq_trans instead since n < m is just a notation for n.+1 <= m (c.f., comment in util/nat.v).")]
-  Lemma ltn_leq_trans n m p : m < n -> n <= p -> m < p.
-  Proof. exact (@leq_trans n m.+1 p). Qed.
-
-End NatOrderLemmas.
+   Nonetheless we introduce it here because an additional (even though
+   arguably redundant) lemma doesn't hurt, and for newcomers the apparent
+   absence of the mirror case of [leq_ltn_trans] can be somewhat confusing.  *)
+#[deprecated(since="0.4",note="Use leq_trans instead since n < m is just a notation for n.+1 <= m (c.f., comment in util/nat.v).")]
+Lemma ltn_leq_trans [n m p] : m < n -> n <= p -> m < p.
+Proof. exact: leq_trans. Qed.
-- 
GitLab