From c6fc2bd6db9b838d85a8f3dbbf7d5ce3ce892c10 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 21 Jun 2023 09:46:16 +0100
Subject: [PATCH 01/80] towards issue #1998: `Data.Nat.Base`; `CHANGELOG`

---
 CHANGELOG.md           |  9 +++++++++
 src/Data/Nat/Base.agda | 31 ++++++++++++++++++++++++++++++-
 2 files changed, 39 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 25bc7bd058..1040d1f081 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2155,9 +2155,18 @@ Other minor changes
   pattern z<s {n}         = s≤s (z≤n {n})
   pattern s<s {m} {n} m<n = s≤s {m} {n} m<n
 
+  s≤s⁻¹ : suc m ≤ suc n → m ≤ n
+  s<s⁻¹ : ∀ {m n} → suc m < suc n → m < n
+
+  LessThan : Rel ℕ 0ℓ
+  <-lessThan   : .(m < n) → LessThan m n
+  <-lessThan⁻¹ : .{{LessThan m n}} → m < n
+
   pattern <′-base          = ≤′-refl
   pattern <′-step {n} m<′n = ≤′-step {n} m<′n
 
+  pattern ≤″-offset k = less-than-or-equal {k} refl
+
   _⊔′_ : ℕ → ℕ → ℕ
   _⊓′_ : ℕ → ℕ → ℕ
   ∣_-_∣′ : ℕ → ℕ → ℕ
diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda
index 4920e7751e..48221d2d00 100644
--- a/src/Data/Nat/Base.agda
+++ b/src/Data/Nat/Base.agda
@@ -60,6 +60,15 @@ m < n = suc m ≤ n
 pattern z<s {n}         = s≤s (z≤n {n})
 pattern s<s {m} {n} m<n = s≤s {m} {n} m<n
 
+-- Smart destructors of _≤_, _<_
+
+s≤s⁻¹ : ∀ {m n} → suc m ≤ suc n → m ≤ n
+s≤s⁻¹ (s≤s m≤n) = m≤n
+
+s<s⁻¹ : ∀ {m n} → suc m < suc n → m < n
+s<s⁻¹ (s<s m<n) = m<n
+
+
 ------------------------------------------------------------------------
 -- other ordering relations
 
@@ -120,11 +129,29 @@ instance
 >-nonZero⁻¹ (suc n) = z<s
 
 ------------------------------------------------------------------------
--- Arithmetic
+-- Another useful (proof-irrelevant) ordering relation
 
 open import Agda.Builtin.Nat public
   using (_+_; _*_) renaming (_-_ to _∸_)
 
+LessThan : Rel ℕ 0ℓ
+LessThan m n = NonZero (n ∸ m)
+
+-- Constructor
+
+<-lessThan : ∀ {m n} → .(m < n) → LessThan m n
+<-lessThan {zero}  {suc n} _   = _
+<-lessThan {suc m} {suc n} m<n = <-lessThan {m} {n} (s<s⁻¹ m<n)
+
+-- Destructor
+
+<-lessThan⁻¹ : ∀ m n → .{{LessThan m n}} → m < n
+<-lessThan⁻¹ zero    (suc n)        = z<s
+<-lessThan⁻¹ (suc m) (suc n) {{lt}} = s<s (<-lessThan⁻¹ m n {{lt}})
+
+------------------------------------------------------------------------
+-- Arithmetic
+
 open import Agda.Builtin.Nat
   using (div-helper; mod-helper)
 
@@ -267,6 +294,8 @@ record _≤″_ (m n : ℕ) : Set where
     {k}   : ℕ
     proof : m + k ≡ n
 
+pattern ≤″-offset k = less-than-or-equal {k} refl
+
 infix 4 _≤″_ _<″_ _≥″_ _>″_
 
 _<″_ : Rel ℕ 0ℓ

From dd0165f778284680dc680b321757f0f7f46303aa Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 21 Jun 2023 09:54:15 +0100
Subject: [PATCH 02/80] tidied up `CHANGELOG`

---
 CHANGELOG.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1040d1f081..0738cdf0b9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2156,7 +2156,7 @@ Other minor changes
   pattern s<s {m} {n} m<n = s≤s {m} {n} m<n
 
   s≤s⁻¹ : suc m ≤ suc n → m ≤ n
-  s<s⁻¹ : ∀ {m n} → suc m < suc n → m < n
+  s<s⁻¹ : suc m < suc n → m < n
 
   LessThan : Rel ℕ 0ℓ
   <-lessThan   : .(m < n) → LessThan m n

From 80a63862c1bd0f7ba9aa7717708376ce89d14167 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 21 Jun 2023 11:53:22 +0100
Subject: [PATCH 03/80] reorganised to push `LessThan` further down the module`

---
 src/Data/Nat/Base.agda | 48 +++++++++++++++++++++---------------------
 1 file changed, 24 insertions(+), 24 deletions(-)

diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda
index 48221d2d00..00d8d1ae3e 100644
--- a/src/Data/Nat/Base.agda
+++ b/src/Data/Nat/Base.agda
@@ -128,32 +128,11 @@ instance
 >-nonZero⁻¹ : ∀ n → .{{NonZero n}} → n > 0
 >-nonZero⁻¹ (suc n) = z<s
 
-------------------------------------------------------------------------
--- Another useful (proof-irrelevant) ordering relation
-
-open import Agda.Builtin.Nat public
-  using (_+_; _*_) renaming (_-_ to _∸_)
-
-LessThan : Rel ℕ 0ℓ
-LessThan m n = NonZero (n ∸ m)
-
--- Constructor
-
-<-lessThan : ∀ {m n} → .(m < n) → LessThan m n
-<-lessThan {zero}  {suc n} _   = _
-<-lessThan {suc m} {suc n} m<n = <-lessThan {m} {n} (s<s⁻¹ m<n)
-
--- Destructor
-
-<-lessThan⁻¹ : ∀ m n → .{{LessThan m n}} → m < n
-<-lessThan⁻¹ zero    (suc n)        = z<s
-<-lessThan⁻¹ (suc m) (suc n) {{lt}} = s<s (<-lessThan⁻¹ m n {{lt}})
-
 ------------------------------------------------------------------------
 -- Arithmetic
 
-open import Agda.Builtin.Nat
-  using (div-helper; mod-helper)
+open import Agda.Builtin.Nat public
+  using (_+_; _*_; div-helper; mod-helper) renaming (_-_ to _∸_)
 
 pred : ℕ → ℕ
 pred n = n ∸ 1
@@ -260,7 +239,28 @@ zero  ! = 1
 suc n ! = suc n * n !
 
 ------------------------------------------------------------------------
--- Alternative definition of _≤_
+-- Alternative definitions of _≤_/_<_
+
+------------------------------------------------------------------------
+-- Another useful (proof-irrelevant) relation
+
+LessThan : Rel ℕ 0ℓ
+LessThan m n = NonZero (n ∸ m)
+
+-- Constructor
+
+<-lessThan : ∀ {m n} → .(m < n) → LessThan m n
+<-lessThan {zero}  {suc n} _   = _
+<-lessThan {suc m} {suc n} m<n = <-lessThan {m} {n} (s<s⁻¹ m<n)
+
+-- Destructor
+
+<-lessThan⁻¹ : ∀ m n → .{{LessThan m n}} → m < n
+<-lessThan⁻¹ zero    (suc n)        = z<s
+<-lessThan⁻¹ (suc m) (suc n) {{lt}} = s<s (<-lessThan⁻¹ m n {{lt}})
+
+------------------------------------------------------------------------
+-- Another alternative definition of _≤_
 
 -- The following definition of _≤_ is more suitable for well-founded
 -- induction (see Data.Nat.Induction)

From a945344ddc3bfb4ce6dadf5907f7ec9fedd74e08 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 22 Jun 2023 08:34:17 +0100
Subject: [PATCH 04/80] =?UTF-8?q?relating=20`LessThan`=20and=20`=5F<?=
 =?UTF-8?q?=E1=B5=87=5F`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Data/Nat/Base.agda | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda
index 00d8d1ae3e..23250b1994 100644
--- a/src/Data/Nat/Base.agda
+++ b/src/Data/Nat/Base.agda
@@ -247,13 +247,21 @@ suc n ! = suc n * n !
 LessThan : Rel ℕ 0ℓ
 LessThan m n = NonZero (n ∸ m)
 
--- Constructor
+-- Constructors
+
+<ᵇ-lessThan : ∀ {m n} → .(T (m <ᵇ n)) → LessThan m n
+<ᵇ-lessThan {zero}  {suc n} _ = _
+<ᵇ-lessThan {suc m} {suc n} m<n = <ᵇ-lessThan {m} {n} m<n
 
 <-lessThan : ∀ {m n} → .(m < n) → LessThan m n
 <-lessThan {zero}  {suc n} _   = _
 <-lessThan {suc m} {suc n} m<n = <-lessThan {m} {n} (s<s⁻¹ m<n)
 
--- Destructor
+-- Destructors
+
+<ᵇ-lessThan⁻¹ : ∀ m n → .{{LessThan m n}} → T (m <ᵇ n)
+<ᵇ-lessThan⁻¹ zero    (suc n) = _
+<ᵇ-lessThan⁻¹ (suc m) (suc n) = <ᵇ-lessThan⁻¹ m n
 
 <-lessThan⁻¹ : ∀ m n → .{{LessThan m n}} → m < n
 <-lessThan⁻¹ zero    (suc n)        = z<s

From 7fc2e5885dbe27c3001f8a09191323d118a1aeae Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 22 Jun 2023 08:36:02 +0100
Subject: [PATCH 05/80] =?UTF-8?q?relating=20`LessThan`=20and=20`=5F<?=
 =?UTF-8?q?=E1=B5=87=5F`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CHANGELOG.md | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 0738cdf0b9..ad04db38d1 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2159,8 +2159,10 @@ Other minor changes
   s<s⁻¹ : suc m < suc n → m < n
 
   LessThan : Rel ℕ 0ℓ
-  <-lessThan   : .(m < n) → LessThan m n
-  <-lessThan⁻¹ : .{{LessThan m n}} → m < n
+  <ᵇ-lessThan   : .(T (m <ᵇ n)) → LessThan m n
+  <-lessThan    : .(m < n) → LessThan m n
+  <ᵇ-lessThan⁻¹ : .{{LessThan m n}} → T (m <ᵇ n)
+  <-lessThan⁻¹  : .{{LessThan m n}} → m < n
 
   pattern <′-base          = ≤′-refl
   pattern <′-step {n} m<′n = ≤′-step {n} m<′n

From 9ad0e7f9a2a2b4edeee85ca92fdadd5e5db7cecf Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 23 Jun 2023 12:50:36 +0100
Subject: [PATCH 06/80] =?UTF-8?q?reverted=20to=20using=20`=5F<=E1=B5=87=5F?=
 =?UTF-8?q?`;=20simplified=20imports?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Data/Fin/Base.agda | 52 ++++++++++++++++++++++++------------------
 src/Data/Nat/Base.agda | 41 ++++++++++++++++++++++-----------
 2 files changed, 58 insertions(+), 35 deletions(-)

diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda
index 20a2636216..b7ce7f5459 100644
--- a/src/Data/Fin/Base.agda
+++ b/src/Data/Fin/Base.agda
@@ -13,13 +13,11 @@ module Data.Fin.Base where
 
 open import Data.Bool.Base using (Bool; true; false; T; not)
 open import Data.Empty using (⊥-elim)
-open import Data.Nat.Base as ℕ using (ℕ; zero; suc; z≤n; s≤s; z<s; s<s; _^_)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
 open import Data.Product as Product using (_×_; _,_; proj₁; proj₂)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (id; _∘_; _on_; flip)
 open import Level using (0ℓ)
-open import Relation.Nullary.Negation.Core using (contradiction)
-open import Relation.Nullary.Decidable.Core using (yes; no; True; toWitness)
 open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong)
 open import Relation.Binary.Indexed.Heterogeneous.Core using (IRel)
@@ -67,18 +65,28 @@ fromℕ : (n : ℕ) → Fin (suc n)
 fromℕ zero    = zero
 fromℕ (suc n) = suc (fromℕ n)
 
+-- fromℕLessThan m ⦃_⦄ = "m".
+
+fromℕLessThan : ∀ m {n} → .{{ℕ.LessThan m n}} → Fin n
+fromℕLessThan zero    {suc _} = zero
+fromℕLessThan (suc m) {suc _} = suc (fromℕLessThan m)
+
 -- fromℕ< {m} _ = "m".
 
-fromℕ< : m ℕ.< n → Fin n
-fromℕ< {zero}  {suc n} z<s = zero
-fromℕ< {suc m} {suc n} (s<s m<n) = suc (fromℕ< m<n)
+fromℕ< : ∀ {m n} → .(m ℕ.< n) → Fin n
+fromℕ< m<n = fromℕLessThan _ where instance _ = ℕ.<-lessThan m<n
+
+-- fromℕ<′ m ⦃_⦄ = "m".
+
+fromℕ<′ : ∀ m {n} → .{{m ℕ.< n}} → Fin n
+fromℕ<′ zero    {suc _} = zero
+fromℕ<′ (suc m) {suc _} ⦃ m<n ⦄ = suc (fromℕ<′ m ⦃ ℕ.s<s⁻¹ m<n ⦄)
 
 -- fromℕ<″ m _ = "m".
 
-fromℕ<″ : ∀ m {n} → m ℕ.<″ n → Fin n
-fromℕ<″ zero    (ℕ.less-than-or-equal refl) = zero
-fromℕ<″ (suc m) (ℕ.less-than-or-equal refl) =
-  suc (fromℕ<″ m (ℕ.less-than-or-equal refl))
+fromℕ<″ : ∀ {m n} → .(m ℕ.<″ n) → Fin n
+fromℕ<″ {zero}  {suc _} _    = zero
+fromℕ<″ {suc m} {suc _} m<″n = suc (fromℕ<″ (ℕ.s<″s⁻¹ m<″n))
 
 -- canonical liftings of i:Fin m to larger index
 
@@ -96,9 +104,9 @@ zero    ↑ʳ i = i
 
 -- reduce≥ "m + i" _ = "i".
 
-reduce≥ : ∀ (i : Fin (m ℕ.+ n)) (i≥m : toℕ i ℕ.≥ m) → Fin n
-reduce≥ {zero}  i       i≥m       = i
-reduce≥ {suc m} (suc i) (s≤s i≥m) = reduce≥ i i≥m
+reduce≥ : ∀ (i : Fin (m ℕ.+ n)) → .(m ℕ.≤ (toℕ i)) → Fin n
+reduce≥ {zero}  i       _   = i
+reduce≥ {suc m} (suc i) m≤i = reduce≥ {m} i (ℕ.s≤s⁻¹ m≤i)
 
 -- inject⋆ m "i" = "i".
 
@@ -107,16 +115,16 @@ inject {i = suc i} zero    = zero
 inject {i = suc i} (suc j) = suc (inject j)
 
 inject! : ∀ {i : Fin (suc n)} → Fin′ i → Fin n
-inject! {n = suc _} {i = suc _}  zero    = zero
-inject! {n = suc _} {i = suc _}  (suc j) = suc (inject! j)
+inject! {n = suc _} {i = suc _} zero    = zero
+inject! {n = suc _} {i = suc _} (suc j) = suc (inject! j)
 
 inject₁ : Fin n → Fin (suc n)
 inject₁ zero    = zero
 inject₁ (suc i) = suc (inject₁ i)
 
-inject≤ : Fin m → m ℕ.≤ n → Fin n
-inject≤ {_} {suc n} zero    _        = zero
-inject≤ {_} {suc n} (suc i) (s≤s m≤n) = suc (inject≤ i m≤n)
+inject≤ : Fin m → .(m ℕ.≤ n) → Fin n
+inject≤ {n = suc _} zero    _   = zero
+inject≤ {n = suc _} (suc i) m≤n = suc (inject≤ i (ℕ.s≤s⁻¹ m≤n))
 
 -- lower₁ "i" _ = "i".
 
@@ -167,12 +175,12 @@ combine {suc m} {n} zero    j = j ↑ˡ (m ℕ.* n)
 combine {suc m} {n} (suc i) j = n ↑ʳ (combine i j)
 
 -- Next in progression after splitAt and remQuot
-finToFun : Fin (m ^ n) → (Fin n → Fin m)
-finToFun {m} {suc n} i zero    = quotient (m ^ n) i
-finToFun {m} {suc n} i (suc j) = finToFun (remainder {m} (m ^ n) i) j
+finToFun : Fin (m ℕ.^ n) → (Fin n → Fin m)
+finToFun {m} {suc n} i zero    = quotient (m ℕ.^ n) i
+finToFun {m} {suc n} i (suc j) = finToFun (remainder {m} (m ℕ.^ n) i) j
 
 -- inverse of above function
-funToFin : (Fin m → Fin n) → Fin (n ^ m)
+funToFin : (Fin m → Fin n) → Fin (n ℕ.^ m)
 funToFin {zero}  f = zero
 funToFin {suc m} f = combine (f zero) (funToFin (f ∘ suc))
 
diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda
index 23250b1994..cbd5fff742 100644
--- a/src/Data/Nat/Base.agda
+++ b/src/Data/Nat/Base.agda
@@ -134,6 +134,9 @@ instance
 open import Agda.Builtin.Nat public
   using (_+_; _*_; div-helper; mod-helper) renaming (_-_ to _∸_)
 
+open import Agda.Builtin.Nat
+  using (div-helper; mod-helper)
+
 pred : ℕ → ℕ
 pred n = n ∸ 1
 
@@ -242,16 +245,18 @@ suc n ! = suc n * n !
 -- Alternative definitions of _≤_/_<_
 
 ------------------------------------------------------------------------
--- Another useful (proof-irrelevant) relation
+-- Another useful (proof-irrelevant) definition of _<_
 
 LessThan : Rel ℕ 0ℓ
-LessThan m n = NonZero (n ∸ m)
+LessThan m n = T (m <ᵇ n)
 
--- Constructors
+-- instance
 
-<ᵇ-lessThan : ∀ {m n} → .(T (m <ᵇ n)) → LessThan m n
-<ᵇ-lessThan {zero}  {suc n} _ = _
-<ᵇ-lessThan {suc m} {suc n} m<n = <ᵇ-lessThan {m} {n} m<n
+instance
+  lessThan : ∀ {n} → LessThan 0 (suc n)
+  lessThan = _
+
+-- Constructors
 
 <-lessThan : ∀ {m n} → .(m < n) → LessThan m n
 <-lessThan {zero}  {suc n} _   = _
@@ -259,13 +264,15 @@ LessThan m n = NonZero (n ∸ m)
 
 -- Destructors
 
-<ᵇ-lessThan⁻¹ : ∀ m n → .{{LessThan m n}} → T (m <ᵇ n)
-<ᵇ-lessThan⁻¹ zero    (suc n) = _
-<ᵇ-lessThan⁻¹ (suc m) (suc n) = <ᵇ-lessThan⁻¹ m n
+<-lessThan⁻¹ : ∀ m {n} → .{{LessThan m n}} → m < n
+<-lessThan⁻¹ zero    {suc n} = z<s
+<-lessThan⁻¹ (suc m) {suc n} = s<s (<-lessThan⁻¹ m)
+
+-- Non-Constructor
+
+¬[n]LessThan[0] : ∀ {n} → ¬ LessThan n 0
+¬[n]LessThan[0] ()
 
-<-lessThan⁻¹ : ∀ m n → .{{LessThan m n}} → m < n
-<-lessThan⁻¹ zero    (suc n)        = z<s
-<-lessThan⁻¹ (suc m) (suc n) {{lt}} = s<s (<-lessThan⁻¹ m n {{lt}})
 
 ------------------------------------------------------------------------
 -- Another alternative definition of _≤_
@@ -302,7 +309,10 @@ record _≤″_ (m n : ℕ) : Set where
     {k}   : ℕ
     proof : m + k ≡ n
 
-pattern ≤″-offset k = less-than-or-equal {k} refl
+-- Smart constructor of _<″_
+
+pattern ≤″-offset k = less-than-or-equal {k = k} refl
+pattern <″-offset k = ≤″-offset k
 
 infix 4 _≤″_ _<″_ _≥″_ _>″_
 
@@ -315,6 +325,11 @@ m ≥″ n = n ≤″ m
 _>″_ : Rel ℕ 0ℓ
 m >″ n = n <″ m
 
+-- Smart destructor of _<″_
+
+s<″s⁻¹ : ∀ {m n} → suc m <″ suc n → m <″ n
+s<″s⁻¹ (<″-offset k) = <″-offset k
+
 ------------------------------------------------------------------------
 -- Another alternative definition of _≤_
 

From 44acc1fba89d83f7907c6d40b2a4059d973be4e4 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 23 Jun 2023 12:54:31 +0100
Subject: [PATCH 07/80] fixed imports

---
 src/Data/Nat/Base.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda
index cbd5fff742..1a6c1d9b36 100644
--- a/src/Data/Nat/Base.agda
+++ b/src/Data/Nat/Base.agda
@@ -132,7 +132,7 @@ instance
 -- Arithmetic
 
 open import Agda.Builtin.Nat public
-  using (_+_; _*_; div-helper; mod-helper) renaming (_-_ to _∸_)
+  using (_+_; _*_) renaming (_-_ to _∸_)
 
 open import Agda.Builtin.Nat
   using (div-helper; mod-helper)

From 426723254a1206b2c8f2dae57049bdd633864faf Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 23 Jun 2023 13:13:18 +0100
Subject: [PATCH 08/80] simplified imports; removed some uses of `with`

---
 src/Data/Nat/Properties.agda | 58 ++++++++++++++++++++----------------
 1 file changed, 33 insertions(+), 25 deletions(-)

diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 27725b98ad..dbf7c2a06c 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -21,7 +21,6 @@ import Algebra.Lattice.Construct.NaturalChoice.MinMaxOp as LatticeMinMaxOp
 import Algebra.Properties.CommutativeSemigroup as CommSemigroupProperties
 open import Data.Bool.Base using (Bool; false; true; T)
 open import Data.Bool.Properties using (T?)
-open import Data.Empty using (⊥)
 open import Data.Nat.Base
 open import Data.Product using (∄; ∃; _×_; _,_)
 open import Data.Sum.Base as Sum
@@ -31,12 +30,12 @@ open import Function.Bundles using (_↣_)
 open import Function.Metric.Nat
 open import Level using (0ℓ)
 open import Relation.Unary as U using (Pred)
-open import Relation.Binary
+open import Relation.Binary as B
 open import Relation.Binary.Consequences using (flip-Connex)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary hiding (Irrelevant)
 open import Relation.Nullary.Decidable using (True; via-injection; map′)
-open import Relation.Nullary.Negation using (contradiction; contradiction₂)
+open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Nullary.Reflects using (fromEquivalence)
 
 open import Algebra.Definitions {A = ℕ} _≡_
@@ -106,6 +105,15 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n))
 1+n≢n : ∀ {n} → suc n ≢ n
 1+n≢n {suc n} = 1+n≢n ∘ suc-injective
 
+------------------------------------------------------------------------
+-- Properties of LessThan
+------------------------------------------------------------------------
+
+lessThan? : B.Decidable LessThan
+lessThan? m       zero    = no (¬[n]LessThan[0] {m})
+lessThan? zero    (suc n) = yes _
+lessThan? (suc m) (suc n) = lessThan? m n
+
 ------------------------------------------------------------------------
 -- Properties of _<ᵇ_
 ------------------------------------------------------------------------
@@ -161,9 +169,7 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n))
 ≤-total : Total _≤_
 ≤-total zero    _       = inj₁ z≤n
 ≤-total _       zero    = inj₂ z≤n
-≤-total (suc m) (suc n) with ≤-total m n
-... | inj₁ m≤n = inj₁ (s≤s m≤n)
-... | inj₂ n≤m = inj₂ (s≤s n≤m)
+≤-total (suc m) (suc n) = [ (inj₁ ∘ s≤s) , (inj₂ ∘ s≤s) ]′ (≤-total m n)
 
 ≤-irrelevant : Irrelevant _≤_
 ≤-irrelevant z≤n        z≤n        = refl
@@ -252,9 +258,6 @@ _≥?_ = flip _≤?_
 s≤s-injective : ∀ {m n} {p q : m ≤ n} → s≤s p ≡ s≤s q → p ≡ q
 s≤s-injective refl = refl
 
-≤-pred : ∀ {m n} → suc m ≤ suc n → m ≤ n
-≤-pred (s≤s m≤n) = m≤n
-
 m≤n⇒m≤1+n : ∀ {m n} → m ≤ n → m ≤ 1 + n
 m≤n⇒m≤1+n z≤n       = z≤n
 m≤n⇒m≤1+n (s≤s m≤n) = s≤s (m≤n⇒m≤1+n m≤n)
@@ -414,9 +417,6 @@ _>?_ = flip _<?_
 s<s-injective : ∀ {m n} {p q : m < n} → s<s p ≡ s<s q → p ≡ q
 s<s-injective refl = refl
 
-<-pred : ∀ {m n} → suc m < suc n → m < n
-<-pred (s<s m<n) = m<n
-
 m<n⇒m<1+n : ∀ {m n} → m < n → m < 1 + n
 m<n⇒m<1+n z<s               = z<s
 m<n⇒m<1+n (s<s m<n@(s≤s _)) = s<s (m<n⇒m<1+n m<n)
@@ -453,11 +453,10 @@ m<n⇒m≤1+n : ∀ {m n} → m < n → m ≤ suc n
 m<n⇒m≤1+n = m≤n⇒m≤1+n ∘ <⇒≤
 
 m<1+n⇒m<n∨m≡n :  ∀ {m n} → m < suc n → m < n ⊎ m ≡ n
-m<1+n⇒m<n∨m≡n {0}     {0}     _          =  inj₂ refl
-m<1+n⇒m<n∨m≡n {0}     {suc n} _          =  inj₁ 0<1+n
-m<1+n⇒m<n∨m≡n {suc m} {suc n} (s<s m<1+n)  with m<1+n⇒m<n∨m≡n m<1+n
-... | inj₂ m≡n = inj₂ (cong suc m≡n)
-... | inj₁ m<n = inj₁ (s<s m<n)
+m<1+n⇒m<n∨m≡n {0}     {0}     _           = inj₂ refl
+m<1+n⇒m<n∨m≡n {0}     {suc n} _           = inj₁ 0<1+n
+m<1+n⇒m<n∨m≡n {suc m} {suc n} (s<s m<1+n)
+  = [ inj₁ ∘ s<s , inj₂ ∘ (cong suc) ]′ (m<1+n⇒m<n∨m≡n m<1+n)
 
 m≤n⇒m<n∨m≡n :  ∀ {m n} → m ≤ n → m < n ⊎ m ≡ n
 m≤n⇒m<n∨m≡n m≤n = m<1+n⇒m<n∨m≡n (s≤s m≤n)
@@ -479,7 +478,7 @@ m<1+n⇒m≤n (s≤s m≤n) = m≤n
 ∀[m<n⇒m≢o]⇒n≤o (suc n) (suc o) m<n⇒m≢o = s≤s (∀[m<n⇒m≢o]⇒n≤o n o rec)
   where
   rec : ∀ {m} → m < n → m ≢ o
-  rec x<m refl = m<n⇒m≢o (s≤s x<m) refl
+  rec x<m refl = m<n⇒m≢o (s<s x<m) refl
 
 ------------------------------------------------------------------------
 -- A module for reasoning about the _≤_ and _<_ relations
@@ -2055,14 +2054,13 @@ m<ᵇ1+m+n m = <⇒<ᵇ (m≤m+n (suc m) _)
 <ᵇ⇒<″ {m} {n} leq = less-than-or-equal (m+[n∸m]≡n (<ᵇ⇒< m n leq))
 
 <″⇒<ᵇ : ∀ {m n} → m <″ n → T (m <ᵇ n)
-<″⇒<ᵇ {m} (less-than-or-equal refl) = <⇒<ᵇ (m≤m+n (suc m) _)
+<″⇒<ᵇ {m} (<″-offset k) = <⇒<ᵇ (m≤m+n (suc m) k)
 
 -- equivalence to _≤_
 
 ≤″⇒≤ : _≤″_ ⇒ _≤_
-≤″⇒≤ {zero}  (less-than-or-equal refl) = z≤n
-≤″⇒≤ {suc m} (less-than-or-equal refl) =
-  s≤s (≤″⇒≤ (less-than-or-equal refl))
+≤″⇒≤ {zero}  (≤″-offset k) = z≤n {k}
+≤″⇒≤ {suc m} (≤″-offset k) = s≤s (≤″⇒≤ (≤″-offset k))
 
 ≤⇒≤″ : _≤_ ⇒ _≤″_
 ≤⇒≤″ = less-than-or-equal ∘ m+[n∸m]≡n
@@ -2079,7 +2077,7 @@ _<″?_ : Decidable _<″_
 m <″? n = map′ <ᵇ⇒<″ <″⇒<ᵇ (T? (m <ᵇ n))
 
 _≤″?_ : Decidable _≤″_
-zero  ≤″? n = yes (less-than-or-equal refl)
+zero  ≤″? n = yes (≤″-offset n)
 suc m ≤″? n = m <″? n
 
 _≥″?_ : Decidable _≥″_
@@ -2091,8 +2089,8 @@ _>″?_ = flip _<″?_
 ≤″-irrelevant : Irrelevant _≤″_
 ≤″-irrelevant {m} (less-than-or-equal eq₁)
                   (less-than-or-equal eq₂)
-  with +-cancelˡ-≡ m _ _ (trans eq₁ (sym eq₂))
-... | refl = cong less-than-or-equal (≡-irrelevant eq₁ eq₂)
+  with refl ← +-cancelˡ-≡ m _ _ (trans eq₁ (sym eq₂))
+  = cong less-than-or-equal (≡-irrelevant eq₁ eq₂)
 
 <″-irrelevant : Irrelevant _<″_
 <″-irrelevant = ≤″-irrelevant
@@ -2289,6 +2287,16 @@ n≤m⊔n = m≤n⊔m
 
 -- Version 2.0
 
+≤-pred = s≤s⁻¹
+{-# WARNING_ON_USAGE ≤-pred
+"Warning: ≤-pred was deprecated in v2.0. Please use Data.Nat.Base.s≤s⁻¹ instead. "
+#-}
+
+<-pred = s<s⁻¹
+{-# WARNING_ON_USAGE ≤-pred
+"Warning: <-pred was deprecated in v2.0. Please use Data.Nat.Base.s<s⁻¹ instead. "
+#-}
+
 suc[pred[n]]≡n : ∀ {n} → n ≢ 0 → suc (pred n) ≡ n
 suc[pred[n]]≡n {zero}  0≢0 = contradiction refl 0≢0
 suc[pred[n]]≡n {suc n} _   = refl

From a97fc28f126781c0eeb275786e3700b491708b5a Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 23 Jun 2023 13:15:14 +0100
Subject: [PATCH 09/80] spurious parentheses

---
 src/Data/Nat/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index dbf7c2a06c..626c9448ec 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -169,7 +169,7 @@ lessThan? (suc m) (suc n) = lessThan? m n
 ≤-total : Total _≤_
 ≤-total zero    _       = inj₁ z≤n
 ≤-total _       zero    = inj₂ z≤n
-≤-total (suc m) (suc n) = [ (inj₁ ∘ s≤s) , (inj₂ ∘ s≤s) ]′ (≤-total m n)
+≤-total (suc m) (suc n) = [ inj₁ ∘ s≤s , inj₂ ∘ s≤s ]′ (≤-total m n)
 
 ≤-irrelevant : Irrelevant _≤_
 ≤-irrelevant z≤n        z≤n        = refl

From b57f651ae27fcf562683ae403259100f4178d7d7 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 23 Jun 2023 13:40:47 +0100
Subject: [PATCH 10/80] new proofs of old properties; old proofs of new
 properties; reinstated non-strict versions

---
 src/Data/Fin/Properties.agda | 165 ++++++++++++++++++++++-------------
 1 file changed, 103 insertions(+), 62 deletions(-)

diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index d7a963f9fd..905b8a0c4e 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -18,11 +18,13 @@ open import Data.Bool.Base using (Bool; true; false; not; _∧_; _∨_)
 open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Fin.Base
 open import Data.Fin.Patterns
-open import Data.Nat.Base as ℕ using (ℕ; zero; suc; s≤s; z≤n; z<s; s<s; _∸_; _^_)
+open import Data.Nat.Base as ℕ
+  using (ℕ; zero; suc; s≤s; z≤n; z<s; s<s; s<s⁻¹; _∸_; _^_)
 import Data.Nat.Properties as ℕₚ
 open import Data.Nat.Solver
 open import Data.Unit using (⊤; tt)
-open import Data.Product using (Σ-syntax; ∃; ∃₂; ∄; _×_; _,_; map; proj₁; proj₂; uncurry; <_,_>)
+open import Data.Product
+  using (Σ-syntax; ∃; ∃₂; ∄; _×_; _,_; map; proj₁; proj₂; uncurry; <_,_>)
 open import Data.Product.Properties using (,-injective)
 open import Data.Product.Algebra using (×-cong)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]; [_,_]′)
@@ -156,16 +158,23 @@ toℕ-↑ʳ (suc n) i = cong suc (toℕ-↑ʳ n i)
 -- toℕ and the ordering relations
 ------------------------------------------------------------------------
 
+toℕ-LessThan : (i : Fin n) → ℕ.LessThan (toℕ i) n
+toℕ-LessThan zero    = _
+toℕ-LessThan (suc i) = toℕ-LessThan i
+
+toℕ<n : (i : Fin n) → toℕ i ℕ.< n
+toℕ<n {n = suc _} i = ℕ.<-lessThan⁻¹ (toℕ i) {{toℕ-LessThan i}}
+
 toℕ≤pred[n] : ∀ (i : Fin n) → toℕ i ℕ.≤ ℕ.pred n
 toℕ≤pred[n] zero                 = z≤n
 toℕ≤pred[n] (suc {n = suc n} i)  = s≤s (toℕ≤pred[n] i)
 
 toℕ≤n : ∀ (i : Fin n) → toℕ i ℕ.≤ n
 toℕ≤n {suc n} i = ℕₚ.m≤n⇒m≤1+n (toℕ≤pred[n] i)
-
+{-
 toℕ<n : ∀ (i : Fin n) → toℕ i ℕ.< n
 toℕ<n {suc n} i = s<s (toℕ≤pred[n] i)
-
+-}
 -- A simpler implementation of toℕ≤pred[n],
 -- however, with a different reduction behavior.
 -- If no one needs the reduction behavior of toℕ≤pred[n],
@@ -198,53 +207,81 @@ fromℕ-toℕ zero    = refl
 fromℕ-toℕ (suc i) = cong suc (fromℕ-toℕ i)
 
 ≤fromℕ : ∀ (i : Fin (ℕ.suc n)) → i ≤ fromℕ n
-≤fromℕ i = subst (toℕ i ℕ.≤_) (sym (toℕ-fromℕ _)) (toℕ≤pred[n] i)
+≤fromℕ {n = n} i rewrite toℕ-fromℕ n = ℕ.s≤s⁻¹ (toℕ<n i)
+
+------------------------------------------------------------------------
+-- fromℕLessThan
+------------------------------------------------------------------------
+
+fromℕLessThan-toℕ : ∀ (i : Fin n) → let instance _ = toℕ-LessThan i in
+                    fromℕLessThan (toℕ i) ≡ i
+fromℕLessThan-toℕ zero    = refl
+fromℕLessThan-toℕ (suc i) = cong suc (fromℕLessThan-toℕ i)
+
+toℕ-fromℕLessThan : ∀ m {n} .{{_ : ℕ.LessThan m n}} → toℕ (fromℕLessThan m {n}) ≡ m
+toℕ-fromℕLessThan zero    {suc _} = refl
+toℕ-fromℕLessThan (suc m) {suc _} = cong suc (toℕ-fromℕLessThan m)
 
 ------------------------------------------------------------------------
 -- fromℕ<
 ------------------------------------------------------------------------
 
-fromℕ<-toℕ : ∀ (i : Fin n) (i<n : toℕ i ℕ.< n) → fromℕ< i<n ≡ i
-fromℕ<-toℕ zero    z<s       = refl
-fromℕ<-toℕ (suc i) (s<s i<n) = cong suc (fromℕ<-toℕ i i<n)
+fromℕ<≡fromℕLessThan : ∀ {m n} .(m<n : m ℕ.< n) →
+                       let instance _ = ℕ.<-lessThan m<n in
+                       fromℕ< m<n ≡ fromℕLessThan m
+fromℕ<≡fromℕLessThan {zero}  {suc _} m<n = refl
+fromℕ<≡fromℕLessThan {suc m} {suc _} m<n = cong suc (fromℕ<≡fromℕLessThan (ℕ.s<s⁻¹ m<n))
+
+fromℕ<-toℕ : (i : Fin n) .(i<n : toℕ i ℕ.< n) → fromℕ< i<n ≡ i
+fromℕ<-toℕ zero    _   = refl
+fromℕ<-toℕ (suc i) i<n = cong suc (fromℕ<-toℕ i (ℕ.s<s⁻¹ i<n))
+
+toℕ-fromℕ< : ∀ {m n} .(m<n : m ℕ.< n) → toℕ (fromℕ< m<n) ≡ m
+toℕ-fromℕ< {zero}  {suc _} _   = refl
+toℕ-fromℕ< {suc m} {suc n} m<n = cong suc (toℕ-fromℕ< (ℕ.s<s⁻¹ m<n))
+
+fromℕ<′-toℕ : (i : Fin n) → let instance _ = toℕ<n i in fromℕ<′ (toℕ i) ≡ i
+fromℕ<′-toℕ zero    = refl
+fromℕ<′-toℕ (suc i) = cong suc (fromℕ<′-toℕ i)
 
-toℕ-fromℕ< : ∀ (m<n : m ℕ.< n) → toℕ (fromℕ< m<n) ≡ m
-toℕ-fromℕ< z<s               = refl
-toℕ-fromℕ< (s<s m<n@(s≤s _)) = cong suc (toℕ-fromℕ< m<n)
+toℕ-fromℕ<′ : ∀ m {n} .{{_ : m ℕ.< n}} → toℕ (fromℕ<′ m) ≡ m
+toℕ-fromℕ<′ zero    {suc _} = refl
+toℕ-fromℕ<′ (suc m) {suc n} {{lt}} = cong suc (toℕ-fromℕ<′ m {n} {{ℕ.s<s⁻¹ lt}})
 
 -- fromℕ is a special case of fromℕ<.
-fromℕ-def : ∀ n → fromℕ n ≡ fromℕ< ℕₚ.≤-refl
+fromℕ-def : ∀ n → fromℕ n ≡ fromℕ< (ℕₚ.n<1+n n)
 fromℕ-def zero    = refl
 fromℕ-def (suc n) = cong suc (fromℕ-def n)
 
 fromℕ<-cong : ∀ m n {o} → m ≡ n → (m<o : m ℕ.< o) (n<o : n ℕ.< o) →
               fromℕ< m<o ≡ fromℕ< n<o
-fromℕ<-cong 0       0       r z<s       z<s  = refl
-fromℕ<-cong (suc _) (suc _) r (s<s m<n) (s<s n<o)
-  = cong suc (fromℕ<-cong _ _ (ℕₚ.suc-injective r) m<n n<o)
+fromℕ<-cong 0       0               r _ _ = refl
+fromℕ<-cong (suc m) (suc n) {suc o} r m<o n<o
+  = cong suc (fromℕ<-cong m n (ℕₚ.suc-injective r) (s<s⁻¹ m<o) (s<s⁻¹ n<o))
 
 fromℕ<-injective : ∀ m n {o} → (m<o : m ℕ.< o) (n<o : n ℕ.< o) →
-                   fromℕ< m<o ≡ fromℕ< n<o → m ≡ n
-fromℕ<-injective 0       0       z<s               z<s r = refl
-fromℕ<-injective (suc _) (suc _) (s<s m<n@(s≤s _)) (s<s n<o@(s≤s _)) r
-  = cong suc (fromℕ<-injective _ _ m<n n<o (suc-injective r))
+                   fromℕ< m<o ≡ fromℕ< n<o →
+                   m ≡ n
+fromℕ<-injective 0       0       z<s       z<s       r = refl
+fromℕ<-injective (suc m) (suc n) (s<s m<o) (s<s n<o) r
+  = cong suc (fromℕ<-injective m n m<o n<o (suc-injective r))
 
 ------------------------------------------------------------------------
 -- fromℕ<″
 ------------------------------------------------------------------------
 
 fromℕ<≡fromℕ<″ : ∀ (m<n : m ℕ.< n) (m<″n : m ℕ.<″ n) →
-                 fromℕ< m<n ≡ fromℕ<″ m m<″n
-fromℕ<≡fromℕ<″ z<s               (ℕ.less-than-or-equal refl) = refl
-fromℕ<≡fromℕ<″ (s<s m<n@(s≤s _)) (ℕ.less-than-or-equal refl) =
-  cong suc (fromℕ<≡fromℕ<″ m<n (ℕ.less-than-or-equal refl))
-
-toℕ-fromℕ<″ : ∀ (m<n : m ℕ.<″ n) → toℕ (fromℕ<″ m m<n) ≡ m
-toℕ-fromℕ<″ {m} {n} m<n = begin
-  toℕ (fromℕ<″ m m<n)  ≡⟨ cong toℕ (sym (fromℕ<≡fromℕ<″ (ℕₚ.≤″⇒≤ m<n) m<n)) ⟩
-  toℕ (fromℕ< _)       ≡⟨ toℕ-fromℕ< (ℕₚ.≤″⇒≤ m<n) ⟩
-  m                    ∎
-  where open ≡-Reasoning
+                 fromℕ< m<n ≡ fromℕ<″ m<″n
+fromℕ<≡fromℕ<″ z<s               (ℕ.<″-offset _) = refl
+fromℕ<≡fromℕ<″ (s<s m<n@(s≤s _)) (ℕ.<″-offset k) =
+  cong suc (fromℕ<≡fromℕ<″ m<n (ℕ.<″-offset k))
+
+toℕ-fromℕ<″ : ∀ (m<″n : m ℕ.<″ n) → toℕ (fromℕ<″ m<″n) ≡ m
+toℕ-fromℕ<″ {m} {n} m<″n = begin
+  toℕ (fromℕ<″ m<″n) ≡⟨ cong toℕ (sym (fromℕ<≡fromℕ<″ m<n m<″n)) ⟩
+  toℕ (fromℕ<  m<n)  ≡⟨ toℕ-fromℕ< m<n ⟩
+  m                  ∎
+  where open ≡-Reasoning ; m<n = ℕₚ.≤″⇒≤ m<″n
 
 ------------------------------------------------------------------------
 -- Properties of cast
@@ -426,10 +463,10 @@ i<1+i = ℕₚ.n<1+n ∘ toℕ
 <⇒≢ i<i refl = ℕₚ.n≮n _ i<i
 
 ≤∧≢⇒< : i ≤ j → i ≢ j → i < j
-≤∧≢⇒< {i = zero}  {zero}  _         0≢0     = contradiction refl 0≢0
-≤∧≢⇒< {i = zero}  {suc j} _         _       = z<s
-≤∧≢⇒< {i = suc i} {suc j} (s≤s i≤j) 1+i≢1+j =
-  s<s (≤∧≢⇒< i≤j (1+i≢1+j ∘ (cong suc)))
+≤∧≢⇒< {i = zero}  {zero}  _         0≢0   = contradiction refl 0≢0
+≤∧≢⇒< {i = zero}  {suc j} _         _     = z<s
+≤∧≢⇒< {i = suc i} {suc j} 1+i≤1+j 1+i≢1+j =
+  s<s (≤∧≢⇒< (ℕ.s≤s⁻¹ 1+i≤1+j) (1+i≢1+j ∘ (cong suc)))
 
 ------------------------------------------------------------------------
 -- inject
@@ -465,11 +502,11 @@ inject₁ℕ≤ = ℕₚ.<⇒≤ ∘ inject₁ℕ<
 ≤̄⇒inject₁< {i = i} i≤j rewrite sym (toℕ-inject₁ i) = s<s i≤j
 
 ℕ<⇒inject₁< : ∀ {i : Fin (ℕ.suc n)} {j : Fin n} → j < i → inject₁ j < i
-ℕ<⇒inject₁< {i = suc i} (s≤s j≤i) = ≤̄⇒inject₁< j≤i
+ℕ<⇒inject₁< {i = suc i} j≤i = ≤̄⇒inject₁< (ℕ.s≤s⁻¹ j≤i)
 
 i≤inject₁[j]⇒i≤1+j : i ≤ inject₁ j → i ≤ suc j
-i≤inject₁[j]⇒i≤1+j {i = zero} i≤j = z≤n
-i≤inject₁[j]⇒i≤1+j {i = suc i} {j = suc j} (s≤s i≤j) = s≤s (ℕₚ.m≤n⇒m≤1+n (subst (toℕ i ℕ.≤_) (toℕ-inject₁ j) i≤j))
+i≤inject₁[j]⇒i≤1+j {i = zero}              _   = z≤n
+i≤inject₁[j]⇒i≤1+j {i = suc i} {j = suc j} i≤j = s≤s (ℕₚ.m≤n⇒m≤1+n (subst (toℕ i ℕ.≤_) (toℕ-inject₁ j) (ℕ.s≤s⁻¹ i≤j)))
 
 ------------------------------------------------------------------------
 -- lower₁
@@ -482,8 +519,8 @@ toℕ-lower₁ {ℕ.suc m} (suc i) p = cong ℕ.suc (toℕ-lower₁ i (p ∘ con
 
 lower₁-injective : ∀ {n≢i : n ≢ toℕ i} {n≢j : n ≢ toℕ j} →
                    lower₁ i n≢i ≡ lower₁ j n≢j → i ≡ j
-lower₁-injective {zero}  {zero}  {_}     {n≢i} {_}   _    = ⊥-elim (n≢i refl)
-lower₁-injective {zero}  {_}     {zero}  {_}   {n≢j} _    = ⊥-elim (n≢j refl)
+lower₁-injective {zero}  {zero}  {_}     {n≢i} {_}   _    = contradiction refl n≢i
+lower₁-injective {zero}  {_}     {zero}  {_}   {n≢j} _    = contradiction refl n≢j
 lower₁-injective {suc n} {zero}  {zero}  {_}   {_}   refl = refl
 lower₁-injective {suc n} {suc i} {suc j} {n≢i} {n≢j} eq   =
   cong suc (lower₁-injective (suc-injective eq))
@@ -523,26 +560,26 @@ inject₁≡⇒lower₁≡ n≢j i≡j = inject₁-injective (trans (inject₁-l
 -- inject≤
 ------------------------------------------------------------------------
 
-toℕ-inject≤ : ∀ i (m≤n : m ℕ.≤ n) → toℕ (inject≤ i m≤n) ≡ toℕ i
+toℕ-inject≤ : ∀ i .(m≤n : m ℕ.≤ n) → toℕ (inject≤ i m≤n) ≡ toℕ i
 toℕ-inject≤ {_} {suc n} zero    _         = refl
-toℕ-inject≤ {_} {suc n} (suc i) (s≤s m≤n) = cong suc (toℕ-inject≤ i m≤n)
+toℕ-inject≤ {_} {suc n} (suc i) m≤n = cong suc (toℕ-inject≤ i (ℕ.s≤s⁻¹ m≤n))
 
-inject≤-refl : ∀ i (n≤n : n ℕ.≤ n) → inject≤ i n≤n ≡ i
-inject≤-refl {suc n} zero    _         = refl
-inject≤-refl {suc n} (suc i) (s≤s n≤n) = cong suc (inject≤-refl i n≤n)
+inject≤-refl : ∀ i .(n≤n : n ℕ.≤ n) → inject≤ i n≤n ≡ i
+inject≤-refl {suc n} zero    _   = refl
+inject≤-refl {suc n} (suc i) n≤n = cong suc (inject≤-refl i (ℕ.s≤s⁻¹ n≤n))
 
 inject≤-idempotent : ∀ (i : Fin m)
-                     (m≤n : m ℕ.≤ n) (n≤o : n ℕ.≤ o) (m≤o : m ℕ.≤ o) →
+                     .(m≤n : m ℕ.≤ n) .(n≤o : n ℕ.≤ o) .(m≤o : m ℕ.≤ o) →
                      inject≤ (inject≤ i m≤n) n≤o ≡ inject≤ i m≤o
-inject≤-idempotent {_} {suc n} {suc o} zero    _   _   _ = refl
-inject≤-idempotent {_} {suc n} {suc o} (suc i) (s≤s m≤n) (s≤s n≤o) (s≤s m≤o) =
-  cong suc (inject≤-idempotent i m≤n n≤o m≤o)
+inject≤-idempotent {_} {suc n} {suc o} zero    _   _   _   = refl
+inject≤-idempotent {_} {suc n} {suc o} (suc i) m≤n n≤o m≤o =
+  cong suc (inject≤-idempotent i (ℕ.s≤s⁻¹ m≤n) (ℕ.s≤s⁻¹ n≤o) (ℕ.s≤s⁻¹ m≤o))
 
-inject≤-injective : ∀ (m≤n m≤n′ : m ℕ.≤ n) i j →
+inject≤-injective : ∀ .(m≤n m≤n′ : m ℕ.≤ n) i j →
                     inject≤ i m≤n ≡ inject≤ j m≤n′ → i ≡ j
-inject≤-injective (s≤s p) (s≤s q) zero    zero    eq = refl
-inject≤-injective (s≤s p) (s≤s q) (suc i) (suc j) eq =
-  cong suc (inject≤-injective p q i j (suc-injective eq))
+inject≤-injective {n = suc _} p q zero    zero    eq = refl
+inject≤-injective {n = suc _} p q (suc i) (suc j) eq =
+  cong suc (inject≤-injective (ℕ.s≤s⁻¹ p) (ℕ.s≤s⁻¹ q) i j (suc-injective eq))
 
 ------------------------------------------------------------------------
 -- pred
@@ -592,17 +629,21 @@ join-splitAt (suc m) n (suc i) = begin
 
 -- splitAt "m" "i" ≡ inj₁ "i" if i < m
 
-splitAt-< : ∀ m {n} (i : Fin (m ℕ.+ n)) (i<m : toℕ i ℕ.< m) →
+splitAt-LessThan : ∀ m {n} (i : Fin (m ℕ.+ n)) .{{_ : ℕ.LessThan (toℕ i) m}} →
+            splitAt m i ≡ inj₁ (fromℕLessThan (toℕ i))
+splitAt-LessThan (suc m) zero    = refl
+splitAt-LessThan (suc m) (suc i) = cong (Sum.map suc id) (splitAt-LessThan m i)
+
+splitAt-< : ∀ m {n} (i : Fin (m ℕ.+ n)) .(i<m : toℕ i ℕ.< m) →
             splitAt m i ≡ inj₁ (fromℕ< i<m)
-splitAt-< (suc m) zero    z<s               = refl
-splitAt-< (suc m) (suc i) (s<s i<m) = cong (Sum.map suc id) (splitAt-< m i i<m)
+splitAt-< m i i<m = splitAt-LessThan m i ⦃ ℕ.<-lessThan i<m ⦄
 
 -- splitAt "m" "i" ≡ inj₂ "i - m" if i ≥ m
 
-splitAt-≥ : ∀ m {n} (i : Fin (m ℕ.+ n)) (i≥m : toℕ i ℕ.≥ m) →
+splitAt-≥ : ∀ m {n} (i : Fin (m ℕ.+ n)) .(i≥m : toℕ i ℕ.≥ m) →
             splitAt m i ≡ inj₂ (reduce≥ i i≥m)
-splitAt-≥ zero    i       _         = refl
-splitAt-≥ (suc m) (suc i) (s≤s i≥m) = cong (Sum.map suc id) (splitAt-≥ m i i≥m)
+splitAt-≥ zero    i       _   = refl
+splitAt-≥ (suc m) (suc i) i≥m = cong (Sum.map suc id) (splitAt-≥ m i (ℕ.s≤s⁻¹ i≥m))
 
 ------------------------------------------------------------------------
 -- Bundles
@@ -873,10 +914,10 @@ pinch-surjective zero    (suc j) = suc (suc j) , refl
 pinch-surjective (suc i) (suc j) = map suc (cong suc) (pinch-surjective i j)
 
 pinch-mono-≤ : ∀ (i : Fin n) → (pinch i) Preserves _≤_ ⟶ _≤_
-pinch-mono-≤ 0F      {0F}    {k}     0≤n       = z≤n
-pinch-mono-≤ 0F      {suc j} {suc k} (s≤s j≤k) = j≤k
-pinch-mono-≤ (suc i) {0F}    {k}     0≤n       = z≤n
-pinch-mono-≤ (suc i) {suc j} {suc k} (s≤s j≤k) = s≤s (pinch-mono-≤ i j≤k)
+pinch-mono-≤ 0F      {0F}    {k}     0≤n = z≤n
+pinch-mono-≤ 0F      {suc j} {suc k} j≤k = (ℕ.s≤s⁻¹ j≤k)
+pinch-mono-≤ (suc i) {0F}    {k}     0≤n = z≤n
+pinch-mono-≤ (suc i) {suc j} {suc k} j≤k = s≤s (pinch-mono-≤ i (ℕ.s≤s⁻¹ j≤k))
 
 pinch-injective : ∀ {i : Fin n} {j k : Fin (ℕ.suc n)} →
                   suc i ≢ j → suc i ≢ k → pinch i j ≡ pinch i k → j ≡ k

From 4177542004e382f66a9a0349223ecb1d97575e2b Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 23 Jun 2023 14:48:32 +0100
Subject: [PATCH 11/80] streamlining

---
 src/Data/Fin/Properties.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 905b8a0c4e..3486d2269c 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -278,7 +278,7 @@ fromℕ<≡fromℕ<″ (s<s m<n@(s≤s _)) (ℕ.<″-offset k) =
 
 toℕ-fromℕ<″ : ∀ (m<″n : m ℕ.<″ n) → toℕ (fromℕ<″ m<″n) ≡ m
 toℕ-fromℕ<″ {m} {n} m<″n = begin
-  toℕ (fromℕ<″ m<″n) ≡⟨ cong toℕ (sym (fromℕ<≡fromℕ<″ m<n m<″n)) ⟩
+  toℕ (fromℕ<″ m<″n) ≡˘⟨ cong toℕ (fromℕ<≡fromℕ<″ m<n m<″n) ⟩
   toℕ (fromℕ<  m<n)  ≡⟨ toℕ-fromℕ< m<n ⟩
   m                  ∎
   where open ≡-Reasoning ; m<n = ℕₚ.≤″⇒≤ m<″n
@@ -1110,7 +1110,7 @@ opposite-suc {n} i = begin
   toℕ (opposite (suc i))     ≡⟨ opposite-prop (suc i) ⟩
   suc n ∸ suc (toℕ (suc i))  ≡⟨⟩
   n ∸ toℕ (suc i)            ≡⟨⟩
-  n ∸ suc (toℕ i)            ≡⟨ sym (opposite-prop i) ⟩
+  n ∸ suc (toℕ i)            ≡˘⟨ opposite-prop i ⟩
   toℕ (opposite i)           ∎
   where open ≡-Reasoning
 

From a36b9b4ef4d968d4aea49e683ab956f01beb7949 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 23 Jun 2023 15:19:14 +0100
Subject: [PATCH 12/80] premature deprecation considered harmful

---
 src/Data/Nat/Properties.agda | 14 ++++----------
 1 file changed, 4 insertions(+), 10 deletions(-)

diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 626c9448ec..0f6da4571a 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -155,6 +155,8 @@ lessThan? (suc m) (suc n) = lessThan? m n
 ≤-reflexive {zero}  refl = z≤n
 ≤-reflexive {suc m} refl = s≤s (≤-reflexive refl)
 
+≤-pred = s≤s⁻¹
+
 ≤-refl : Reflexive _≤_
 ≤-refl = ≤-reflexive refl
 
@@ -417,6 +419,8 @@ _>?_ = flip _<?_
 s<s-injective : ∀ {m n} {p q : m < n} → s<s p ≡ s<s q → p ≡ q
 s<s-injective refl = refl
 
+<-pred = s<s⁻¹
+
 m<n⇒m<1+n : ∀ {m n} → m < n → m < 1 + n
 m<n⇒m<1+n z<s               = z<s
 m<n⇒m<1+n (s<s m<n@(s≤s _)) = s<s (m<n⇒m<1+n m<n)
@@ -2287,16 +2291,6 @@ n≤m⊔n = m≤n⊔m
 
 -- Version 2.0
 
-≤-pred = s≤s⁻¹
-{-# WARNING_ON_USAGE ≤-pred
-"Warning: ≤-pred was deprecated in v2.0. Please use Data.Nat.Base.s≤s⁻¹ instead. "
-#-}
-
-<-pred = s<s⁻¹
-{-# WARNING_ON_USAGE ≤-pred
-"Warning: <-pred was deprecated in v2.0. Please use Data.Nat.Base.s<s⁻¹ instead. "
-#-}
-
 suc[pred[n]]≡n : ∀ {n} → n ≢ 0 → suc (pred n) ≡ n
 suc[pred[n]]≡n {zero}  0≢0 = contradiction refl 0≢0
 suc[pred[n]]≡n {suc n} _   = refl

From 4f8e2f2d175797f210e0d97a491a2b68d196c5ea Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 23 Jun 2023 16:40:31 +0100
Subject: [PATCH 13/80] =?UTF-8?q?tidied=20up=20`from=E2=84=95*`=20lemmas?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Data/Fin/Base.agda       | 19 +++++++++----------
 src/Data/Fin/Properties.agda | 10 +++++-----
 2 files changed, 14 insertions(+), 15 deletions(-)

diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda
index b7ce7f5459..832adcbb31 100644
--- a/src/Data/Fin/Base.agda
+++ b/src/Data/Fin/Base.agda
@@ -71,22 +71,21 @@ fromℕLessThan : ∀ m {n} → .{{ℕ.LessThan m n}} → Fin n
 fromℕLessThan zero    {suc _} = zero
 fromℕLessThan (suc m) {suc _} = suc (fromℕLessThan m)
 
--- fromℕ< {m} _ = "m".
-
-fromℕ< : ∀ {m n} → .(m ℕ.< n) → Fin n
-fromℕ< m<n = fromℕLessThan _ where instance _ = ℕ.<-lessThan m<n
-
 -- fromℕ<′ m ⦃_⦄ = "m".
 
 fromℕ<′ : ∀ m {n} → .{{m ℕ.< n}} → Fin n
-fromℕ<′ zero    {suc _} = zero
-fromℕ<′ (suc m) {suc _} ⦃ m<n ⦄ = suc (fromℕ<′ m ⦃ ℕ.s<s⁻¹ m<n ⦄)
+fromℕ<′ m {n} ⦃ m<n ⦄ = fromℕLessThan m where instance _ = ℕ.<-lessThan m<n
+
+-- fromℕ< {m} _ = "m".
+
+fromℕ< : ∀ {m n} → .(m ℕ.< n) → Fin n
+fromℕ< {m} m<n = fromℕ<′ m ⦃ m<n ⦄
 
 -- fromℕ<″ m _ = "m".
 
-fromℕ<″ : ∀ {m n} → .(m ℕ.<″ n) → Fin n
-fromℕ<″ {zero}  {suc _} _    = zero
-fromℕ<″ {suc m} {suc _} m<″n = suc (fromℕ<″ (ℕ.s<″s⁻¹ m<″n))
+fromℕ<″ : ∀ m {n} → .(m ℕ.<″ n) → Fin n
+fromℕ<″ zero    {suc _} _    = zero
+fromℕ<″ (suc m) {suc _} m<″n = suc (fromℕ<″ m (ℕ.s<″s⁻¹ m<″n))
 
 -- canonical liftings of i:Fin m to larger index
 
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 3486d2269c..d6584cdc7d 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -271,16 +271,16 @@ fromℕ<-injective (suc m) (suc n) (s<s m<o) (s<s n<o) r
 ------------------------------------------------------------------------
 
 fromℕ<≡fromℕ<″ : ∀ (m<n : m ℕ.< n) (m<″n : m ℕ.<″ n) →
-                 fromℕ< m<n ≡ fromℕ<″ m<″n
+                 fromℕ< m<n ≡ fromℕ<″ m m<″n
 fromℕ<≡fromℕ<″ z<s               (ℕ.<″-offset _) = refl
 fromℕ<≡fromℕ<″ (s<s m<n@(s≤s _)) (ℕ.<″-offset k) =
   cong suc (fromℕ<≡fromℕ<″ m<n (ℕ.<″-offset k))
 
-toℕ-fromℕ<″ : ∀ (m<″n : m ℕ.<″ n) → toℕ (fromℕ<″ m<″n) ≡ m
+toℕ-fromℕ<″ : ∀ (m<″n : m ℕ.<″ n) → toℕ (fromℕ<″ m m<″n) ≡ m
 toℕ-fromℕ<″ {m} {n} m<″n = begin
-  toℕ (fromℕ<″ m<″n) ≡˘⟨ cong toℕ (fromℕ<≡fromℕ<″ m<n m<″n) ⟩
-  toℕ (fromℕ<  m<n)  ≡⟨ toℕ-fromℕ< m<n ⟩
-  m                  ∎
+  toℕ (fromℕ<″ m m<″n) ≡˘⟨ cong toℕ (fromℕ<≡fromℕ<″ m<n m<″n) ⟩
+  toℕ (fromℕ<  m<n)    ≡⟨ toℕ-fromℕ< m<n ⟩
+  m                    ∎
   where open ≡-Reasoning ; m<n = ℕₚ.≤″⇒≤ m<″n
 
 ------------------------------------------------------------------------

From ea4da27f18f4d79466ca16e0468f1644a5d4d12b Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 23 Jun 2023 16:41:48 +0100
Subject: [PATCH 14/80] corrected `DivMod` appeals to

---
 src/Data/Nat/DivMod.agda       | 13 ++++++-------
 src/Data/Nat/DivMod/WithK.agda | 18 ++++++++----------
 2 files changed, 14 insertions(+), 17 deletions(-)

diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda
index f2b2d8657e..58414b96c7 100644
--- a/src/Data/Nat/DivMod.agda
+++ b/src/Data/Nat/DivMod.agda
@@ -20,7 +20,6 @@ open import Data.Nat.Properties
 open import Function using (_$_)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary.Decidable using (yes; no)
-open import Relation.Nullary.Decidable using (False; toWitnessFalse)
 
 import Algebra.Properties.CommutativeSemigroup *-commutativeSemigroup as *-CS
 
@@ -461,12 +460,12 @@ _div_ : (dividend divisor : ℕ) .{{_ : NonZero divisor}} → ℕ
 _div_ = _/_
 
 _mod_ : (dividend divisor : ℕ) .{{_ : NonZero divisor}} → Fin divisor
-m mod (suc n) = fromℕ< (m%n<n m (suc n))
+m mod n = fromℕ< (m%n<n m n)
 
 _divMod_ : (dividend divisor : ℕ) .{{_ : NonZero divisor}} →
            DivMod dividend divisor
-m divMod n@(suc n-1) = result (m / n) (m mod n) (begin-equality
-  m                                   ≡⟨  m≡m%n+[m/n]*n m n ⟩
-  m % n                    + [m/n]*n  ≡˘⟨ cong (_+ [m/n]*n) (toℕ-fromℕ< (m%n<n m n)) ⟩
-  toℕ (fromℕ< (m%n<n m n)) + [m/n]*n  ∎)
-  where [m/n]*n = m / n * n
+m divMod n = result (m / n) (m mod n) $ begin-equality
+  m                             ≡⟨  m≡m%n+[m/n]*n m n ⟩
+  m % n              + [m/n]*n  ≡˘⟨ cong (_+ [m/n]*n) (toℕ-fromℕ< lemma) ⟩
+  toℕ (fromℕ< lemma) + [m/n]*n  ∎
+  where [m/n]*n = m / n * n ; lemma = m%n<n m n
diff --git a/src/Data/Nat/DivMod/WithK.agda b/src/Data/Nat/DivMod/WithK.agda
index 458a7eef33..3f6047df60 100644
--- a/src/Data/Nat/DivMod/WithK.agda
+++ b/src/Data/Nat/DivMod/WithK.agda
@@ -8,7 +8,7 @@
 
 module Data.Nat.DivMod.WithK where
 
-open import Data.Nat using (ℕ; NonZero; _+_; _*_; _≟_)
+open import Data.Nat using (ℕ; NonZero; _+_; _*_)
 open import Data.Nat.DivMod hiding (_mod_; _divMod_)
 open import Data.Nat.Properties using (≤⇒≤″)
 open import Data.Nat.WithK
@@ -16,7 +16,7 @@ open import Data.Fin.Base using (Fin; toℕ; fromℕ<″)
 open import Data.Fin.Properties using (toℕ-fromℕ<″)
 open import Function.Base using (_$_)
 open import Relation.Binary.PropositionalEquality
-  using (refl; sym; cong; module ≡-Reasoning)
+  using (cong; module ≡-Reasoning)
 open import Relation.Binary.PropositionalEquality.WithK
 
 open ≡-Reasoning
@@ -27,17 +27,15 @@ infixl 7 _mod_ _divMod_
 -- Certified modulus
 
 _mod_ : (dividend divisor : ℕ) → .{{ _ : NonZero divisor }} → Fin divisor
-a mod n = fromℕ<″ (a % n) (≤″-erase (≤⇒≤″ (m%n<n a n)))
+m mod n = fromℕ<″ (m % n) (≤″-erase (≤⇒≤″ (m%n<n m n)))
 
 ------------------------------------------------------------------------
 -- Returns modulus and division result with correctness proof
 
 _divMod_ : (dividend divisor : ℕ) → .{{ NonZero divisor }} →
            DivMod dividend divisor
-a divMod n = result (a / n) (a mod n) $ ≡-erase $ begin
-  a                                 ≡⟨ m≡m%n+[m/n]*n a n ⟩
-  a % n              + [a/n]*n      ≡⟨ cong (_+ [a/n]*n) (sym (toℕ-fromℕ<″ lemma′)) ⟩
-  toℕ (fromℕ<″ _ lemma′) + [a/n]*n  ∎
-  where
-  lemma′ = ≤″-erase (≤⇒≤″ (m%n<n a n))
-  [a/n]*n = a / n * n
+m divMod n = result (m / n) (m mod n) $ ≡-erase $ begin
+  m                                 ≡⟨ m≡m%n+[m/n]*n m n ⟩
+  m % n                  + [m/n]*n  ≡˘⟨ cong (_+ [m/n]*n) (toℕ-fromℕ<″ lemma″) ⟩
+  toℕ (fromℕ<″ _ lemma″) + [m/n]*n  ∎
+  where [m/n]*n = m / n * n ; lemma″ = ≤″-erase (≤⇒≤″ (m%n<n m n))

From f3fa536e00beae68c504c1304c9656e4296b687b Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 23 Jun 2023 16:42:23 +0100
Subject: [PATCH 15/80] weird unsolved metas bug?

---
 src/Data/Nat/Show/Properties.agda | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/src/Data/Nat/Show/Properties.agda b/src/Data/Nat/Show/Properties.agda
index 739a00c2e4..393b9c9fe1 100644
--- a/src/Data/Nat/Show/Properties.agda
+++ b/src/Data/Nat/Show/Properties.agda
@@ -8,7 +8,7 @@
 
 open import Data.Digit using (showDigit; toDigits)
 open import Data.Digit.Properties using (toDigits-injective; showDigit-injective)
-open import Function using (_∘_)
+open import Function using (_∘_; Injective)
 import Data.List.Properties as Listₚ
 open import Data.Nat.Base using (ℕ)
 open import Data.Nat.Properties using (_≤?_)
@@ -20,7 +20,12 @@ module Data.Nat.Show.Properties where
 
 module _ (base : ℕ) {base≥2 : True (2 ≤? base)} {base≤16 : True (base ≤? 16)} where
 
-  charsInBase-injective : ∀ n m → charsInBase base {base≥2} {base≤16} n ≡ charsInBase base {base≥2} {base≤16} m → n ≡ m
-  charsInBase-injective n m = toDigits-injective base {base≥2} _ _
+  private
+    charsInBase-base         = charsInBase base {base≥2} {base≤16}
+    toDigits-injective-base  = toDigits-injective base {base≥2} {base≥2}
+    showDigit-injective-base = showDigit-injective base {base≤16} {base≤16}
+
+  charsInBase-injective : ∀ n m →  charsInBase-base n ≡ charsInBase-base m → n ≡ m
+  charsInBase-injective n m = toDigits-injective-base _ _
                             ∘ Listₚ.reverse-injective
-                            ∘ Listₚ.map-injective (showDigit-injective _ _ _)
+                            ∘ Listₚ.map-injective (showDigit-injective-base _ _)

From 84d136d6acbd1822e0a87a0d141e1c2a86d514fa Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 23 Jun 2023 16:43:02 +0100
Subject: [PATCH 16/80] towards deprecation; tightened dependencies

---
 src/Data/Vec/Relation/Unary/Linked/Properties.agda | 12 ++++--------
 1 file changed, 4 insertions(+), 8 deletions(-)

diff --git a/src/Data/Vec/Relation/Unary/Linked/Properties.agda b/src/Data/Vec/Relation/Unary/Linked/Properties.agda
index a9604e1e6a..69024b1b51 100644
--- a/src/Data/Vec/Relation/Unary/Linked/Properties.agda
+++ b/src/Data/Vec/Relation/Unary/Linked/Properties.agda
@@ -8,21 +8,17 @@
 
 module Data.Vec.Relation.Unary.Linked.Properties where
 
-open import Data.Bool.Base using (true; false)
 open import Data.Vec.Base as Vec
 open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_)
 import Data.Vec.Relation.Unary.All.Properties as Allₚ
 open import Data.Vec.Relation.Unary.Linked as Linked
   using (Linked; []; [-]; _∷_)
 open import Data.Fin.Base using (zero; suc; _<_)
-open import Data.Nat.Base using (ℕ; zero; suc; NonZero)
-open import Data.Nat.Properties using (<-pred)
+open import Data.Nat.Base using (ℕ; zero; suc; s<s⁻¹)
 open import Level using (Level)
-open import Function.Base using (_∘_; flip; _on_)
-open import Relation.Binary using (Rel; Transitive; DecSetoid)
-open import Relation.Binary.PropositionalEquality using (_≢_)
+open import Function.Base using (_on_)
+open import Relation.Binary using (Rel; Transitive)
 open import Relation.Unary using (Pred; Decidable)
-open import Relation.Nullary.Decidable using (yes; no; does)
 
 private
   variable
@@ -47,7 +43,7 @@ module _ (trans : Transitive R) where
            Linked R xs → i < j →
            R (lookup xs i) (lookup xs j)
   lookup⁺ {i = zero}  {j = suc j} (rx ∷ rxs) i<j = Allₚ.lookup⁺ (Linked⇒All rx rxs) j
-  lookup⁺ {i = suc i} {j = suc j} (_  ∷ rxs) i<j = lookup⁺ rxs (<-pred i<j)
+  lookup⁺ {i = suc i} {j = suc j} (_  ∷ rxs) i<j = lookup⁺ rxs (s<s⁻¹ i<j)
 
 ------------------------------------------------------------------------
 -- Introduction (⁺) and elimination (⁻) rules for vec operations

From e594a90333310152d9f3038ec801ce9f7a9a8b05 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 24 Jun 2023 11:07:56 +0100
Subject: [PATCH 17/80] tweaks

---
 src/Data/Nat/Base.agda | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda
index 1a6c1d9b36..73613d0d42 100644
--- a/src/Data/Nat/Base.agda
+++ b/src/Data/Nat/Base.agda
@@ -258,6 +258,10 @@ instance
 
 -- Constructors
 
+lessThanSuc : ∀ {n} → LessThan n (suc n)
+lessThanSuc {zero}  = _
+lessThanSuc {suc n} = lessThanSuc {n}
+
 <-lessThan : ∀ {m n} → .(m < n) → LessThan m n
 <-lessThan {zero}  {suc n} _   = _
 <-lessThan {suc m} {suc n} m<n = <-lessThan {m} {n} (s<s⁻¹ m<n)

From 779c5bf2b57a8f5f4c56883310dcb66ed2182636 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 24 Jun 2023 13:21:51 +0100
Subject: [PATCH 18/80] made `<-lessThan` more implicit; added constructors;
 removed non-constructor

---
 src/Data/Nat/Base.agda | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda
index 73613d0d42..765865978a 100644
--- a/src/Data/Nat/Base.agda
+++ b/src/Data/Nat/Base.agda
@@ -262,9 +262,13 @@ lessThanSuc : ∀ {n} → LessThan n (suc n)
 lessThanSuc {zero}  = _
 lessThanSuc {suc n} = lessThanSuc {n}
 
-<-lessThan : ∀ {m n} → .(m < n) → LessThan m n
-<-lessThan {zero}  {suc n} _   = _
-<-lessThan {suc m} {suc n} m<n = <-lessThan {m} {n} (s<s⁻¹ m<n)
+<-lessThan : ∀ {m n} → .⦃ m < n ⦄ → LessThan m n
+<-lessThan {zero}  {suc n} = _
+<-lessThan {suc m} {suc n} ⦃ m<n ⦄ = <-lessThan {m} {n} ⦃ s<s⁻¹ m<n ⦄
+
+<″-lessThan : ∀ {m n} → LessThan m (suc m + n)
+<″-lessThan {zero}    = _
+<″-lessThan {suc m} = <″-lessThan {m}
 
 -- Destructors
 
@@ -272,11 +276,6 @@ lessThanSuc {suc n} = lessThanSuc {n}
 <-lessThan⁻¹ zero    {suc n} = z<s
 <-lessThan⁻¹ (suc m) {suc n} = s<s (<-lessThan⁻¹ m)
 
--- Non-Constructor
-
-¬[n]LessThan[0] : ∀ {n} → ¬ LessThan n 0
-¬[n]LessThan[0] ()
-
 
 ------------------------------------------------------------------------
 -- Another alternative definition of _≤_

From 373653c6f38d9c2a9049f628c1963309d67e7b7b Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 24 Jun 2023 13:22:42 +0100
Subject: [PATCH 19/80] knock-on simplification

---
 src/Data/Nat/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 0f6da4571a..feac800985 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -110,7 +110,7 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n))
 ------------------------------------------------------------------------
 
 lessThan? : B.Decidable LessThan
-lessThan? m       zero    = no (¬[n]LessThan[0] {m})
+lessThan? m       zero    = no λ()
 lessThan? zero    (suc n) = yes _
 lessThan? (suc m) (suc n) = lessThan? m n
 

From 91a56623fb3c542cf833dcf50b6fd6c5bb0c5038 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 24 Jun 2023 13:38:14 +0100
Subject: [PATCH 20/80] overdid the instances

---
 src/Data/Nat/Base.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda
index 765865978a..1769efd021 100644
--- a/src/Data/Nat/Base.agda
+++ b/src/Data/Nat/Base.agda
@@ -262,9 +262,9 @@ lessThanSuc : ∀ {n} → LessThan n (suc n)
 lessThanSuc {zero}  = _
 lessThanSuc {suc n} = lessThanSuc {n}
 
-<-lessThan : ∀ {m n} → .⦃ m < n ⦄ → LessThan m n
-<-lessThan {zero}  {suc n} = _
-<-lessThan {suc m} {suc n} ⦃ m<n ⦄ = <-lessThan {m} {n} ⦃ s<s⁻¹ m<n ⦄
+<-lessThan : ∀ {m n} → .{m<n : m < n} → LessThan m n
+<-lessThan {zero}  {suc n}         = _
+<-lessThan {suc m} {suc n} {m<n} = <-lessThan {m} {n} {s<s⁻¹ m<n}
 
 <″-lessThan : ∀ {m n} → LessThan m (suc m + n)
 <″-lessThan {zero}    = _

From f2b23ba8f0427e986a5e3f0be897857e4722ae49 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 24 Jun 2023 15:15:14 +0100
Subject: [PATCH 21/80] final (?) reconsideration

---
 src/Data/Nat/Base.agda | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda
index 1769efd021..9b960da60f 100644
--- a/src/Data/Nat/Base.agda
+++ b/src/Data/Nat/Base.agda
@@ -262,9 +262,9 @@ lessThanSuc : ∀ {n} → LessThan n (suc n)
 lessThanSuc {zero}  = _
 lessThanSuc {suc n} = lessThanSuc {n}
 
-<-lessThan : ∀ {m n} → .{m<n : m < n} → LessThan m n
-<-lessThan {zero}  {suc n}         = _
-<-lessThan {suc m} {suc n} {m<n} = <-lessThan {m} {n} {s<s⁻¹ m<n}
+<-lessThan : ∀ {m n} → .(m<n : m < n) → LessThan m n
+<-lessThan {zero}  {suc n}       = _
+<-lessThan {suc m} {suc n} (m<n) = <-lessThan {m} {n} (s<s⁻¹ m<n)
 
 <″-lessThan : ∀ {m n} → LessThan m (suc m + n)
 <″-lessThan {zero}    = _
@@ -272,7 +272,7 @@ lessThanSuc {suc n} = lessThanSuc {n}
 
 -- Destructors
 
-<-lessThan⁻¹ : ∀ m {n} → .{{LessThan m n}} → m < n
+<-lessThan⁻¹ : ∀ m {n} → .⦃ LessThan m n ⦄ → m < n
 <-lessThan⁻¹ zero    {suc n} = z<s
 <-lessThan⁻¹ (suc m) {suc n} = s<s (<-lessThan⁻¹ m)
 

From 4c8f5bbc582570b02ccbe21b2d4b5aac6288223a Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 24 Jun 2023 15:15:36 +0100
Subject: [PATCH 22/80] final (?) reconsideration

---
 src/Data/Fin/Base.agda | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda
index 832adcbb31..a453649c5f 100644
--- a/src/Data/Fin/Base.agda
+++ b/src/Data/Fin/Base.agda
@@ -67,14 +67,15 @@ fromℕ (suc n) = suc (fromℕ n)
 
 -- fromℕLessThan m ⦃_⦄ = "m".
 
-fromℕLessThan : ∀ m {n} → .{{ℕ.LessThan m n}} → Fin n
+fromℕLessThan : ∀ m {n} → .⦃ ℕ.LessThan m n ⦄ → Fin n
 fromℕLessThan zero    {suc _} = zero
 fromℕLessThan (suc m) {suc _} = suc (fromℕLessThan m)
 
 -- fromℕ<′ m ⦃_⦄ = "m".
 
-fromℕ<′ : ∀ m {n} → .{{m ℕ.< n}} → Fin n
-fromℕ<′ m {n} ⦃ m<n ⦄ = fromℕLessThan m where instance _ = ℕ.<-lessThan m<n
+fromℕ<′ : ∀ m {n} → .⦃ m ℕ.< n ⦄ → Fin n
+fromℕ<′ m {n} ⦃ m<n ⦄ = fromℕLessThan m {n}
+  where instance _ = ℕ.<-lessThan m<n
 
 -- fromℕ< {m} _ = "m".
 

From b99b2651d8dc416f9f37158cfad23784b95ce6df Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 24 Jun 2023 15:16:21 +0100
Subject: [PATCH 23/80] final (?) refactoring

---
 src/Data/Fin/Properties.agda | 142 ++++++++++++++++++++++++-----------
 1 file changed, 99 insertions(+), 43 deletions(-)

diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index d6584cdc7d..7da1e082f4 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -163,7 +163,7 @@ toℕ-LessThan zero    = _
 toℕ-LessThan (suc i) = toℕ-LessThan i
 
 toℕ<n : (i : Fin n) → toℕ i ℕ.< n
-toℕ<n {n = suc _} i = ℕ.<-lessThan⁻¹ (toℕ i) {{toℕ-LessThan i}}
+toℕ<n {n = suc _} i = ℕ.<-lessThan⁻¹ (toℕ i) ⦃ toℕ-LessThan i ⦄
 
 toℕ≤pred[n] : ∀ (i : Fin n) → toℕ i ℕ.≤ ℕ.pred n
 toℕ≤pred[n] zero                 = z≤n
@@ -206,7 +206,7 @@ fromℕ-toℕ : ∀ (i : Fin n) → fromℕ (toℕ i) ≡ strengthen i
 fromℕ-toℕ zero    = refl
 fromℕ-toℕ (suc i) = cong suc (fromℕ-toℕ i)
 
-≤fromℕ : ∀ (i : Fin (ℕ.suc n)) → i ≤ fromℕ n
+≤fromℕ : ∀ (i : Fin (suc n)) → i ≤ fromℕ n
 ≤fromℕ {n = n} i rewrite toℕ-fromℕ n = ℕ.s≤s⁻¹ (toℕ<n i)
 
 ------------------------------------------------------------------------
@@ -218,70 +218,126 @@ fromℕLessThan-toℕ : ∀ (i : Fin n) → let instance _ = toℕ-LessThan i in
 fromℕLessThan-toℕ zero    = refl
 fromℕLessThan-toℕ (suc i) = cong suc (fromℕLessThan-toℕ i)
 
-toℕ-fromℕLessThan : ∀ m {n} .{{_ : ℕ.LessThan m n}} → toℕ (fromℕLessThan m {n}) ≡ m
+toℕ-fromℕLessThan : ∀ m {n} .⦃ _ : ℕ.LessThan m n ⦄ → toℕ (fromℕLessThan m {n}) ≡ m
 toℕ-fromℕLessThan zero    {suc _} = refl
 toℕ-fromℕLessThan (suc m) {suc _} = cong suc (toℕ-fromℕLessThan m)
 
+fromℕLessThan-cong : ∀ {m n o} ⦃ m<o : ℕ.LessThan m o ⦄ ⦃ n<o : ℕ.LessThan n o ⦄ →
+                     m ≡ n → fromℕLessThan m {o} ⦃ m<o ⦄ ≡ fromℕLessThan n {o} ⦃ n<o ⦄
+fromℕLessThan-cong {zero}  {zero}                          r = refl
+fromℕLessThan-cong {suc m} {suc n} {suc _} ⦃ m<o ⦄ ⦃ n<o ⦄ r
+  = cong suc (fromℕLessThan-cong {m} {n} ⦃ m<o ⦄ ⦃ n<o ⦄ (ℕₚ.suc-injective r))
+
+fromℕLessThan-injective : ∀ {m n o} ⦃ m<o : ℕ.LessThan m o ⦄ ⦃ n<o : ℕ.LessThan n o ⦄ →
+                          fromℕLessThan m {o} ⦃ m<o ⦄ ≡ fromℕLessThan n {o} ⦃ n<o ⦄ →
+                          m ≡ n
+fromℕLessThan-injective {zero}  {zero}          r = refl
+fromℕLessThan-injective {zero}  {suc n} {suc _} ()
+fromℕLessThan-injective {suc m} {suc n} {suc _} ⦃ m<o ⦄ ⦃ n<o ⦄ r
+  = cong suc (fromℕLessThan-injective {m} {n} ⦃ m<o ⦄ ⦃ n<o ⦄ (suc-injective r))
+
+-- fromℕ is a special case of fromℕLessThan.
+fromℕ-LessThan-def : ∀ n → let instance _ = ℕ.lessThanSuc {n} in
+                     fromℕ n ≡ fromℕLessThan n
+fromℕ-LessThan-def zero    = refl
+fromℕ-LessThan-def (suc n) = cong suc (fromℕ-LessThan-def n)
+
+------------------------------------------------------------------------
+-- fromℕ<′
+------------------------------------------------------------------------
+
+fromℕ<′≡fromℕLessThan : ∀ {m n} → .⦃ m<n : m ℕ.< n ⦄ →
+                        let instance _ = ℕ.<-lessThan m<n in
+                        fromℕ<′ m ≡ fromℕLessThan m
+fromℕ<′≡fromℕLessThan = refl
+
+fromℕ<′-toℕ : (i : Fin n) → let instance _ = toℕ<n i in fromℕ<′ (toℕ i) ≡ i
+fromℕ<′-toℕ i = fromℕLessThan-toℕ i
+
+toℕ-fromℕ<′ : ∀ m {n} .⦃ m<n : m ℕ.< n ⦄ → toℕ (fromℕ<′ m ⦃ m<n ⦄) ≡ m
+toℕ-fromℕ<′ m {n} ⦃ m<n ⦄ = toℕ-fromℕLessThan m {n} ⦃ ℕ.<-lessThan m<n ⦄
+
+fromℕ<′-cong : ∀ {m n o} .⦃ m<o : m ℕ.< o ⦄ .⦃ n<o : n ℕ.< o ⦄ →
+               m ≡ n → fromℕ<′ m ≡ fromℕ<′ n
+fromℕ<′-cong ⦃ m<o ⦄ ⦃ n<o ⦄ r = fromℕLessThan-cong r
+  where
+    instance _ = ℕ.<-lessThan m<o
+    instance _ = ℕ.<-lessThan n<o
+
+fromℕ<′-injective : ∀ {m n o} ⦃ m<o : m ℕ.< o ⦄ ⦃ n<o : n ℕ.< o ⦄ →
+                    fromℕ<′ m {o} ⦃ m<o ⦄ ≡ fromℕ<′ n {o} ⦃ n<o ⦄ →
+                    m ≡ n
+fromℕ<′-injective ⦃ m<o ⦄ ⦃ n<o ⦄ r = fromℕLessThan-injective r
+  where
+    instance _ = ℕ.<-lessThan m<o
+    instance _ = ℕ.<-lessThan n<o
+
 ------------------------------------------------------------------------
 -- fromℕ<
 ------------------------------------------------------------------------
 
-fromℕ<≡fromℕLessThan : ∀ {m n} .(m<n : m ℕ.< n) →
+fromℕ<≡fromℕLessThan : .⦃ m<n : m ℕ.< n ⦄ →
                        let instance _ = ℕ.<-lessThan m<n in
                        fromℕ< m<n ≡ fromℕLessThan m
-fromℕ<≡fromℕLessThan {zero}  {suc _} m<n = refl
-fromℕ<≡fromℕLessThan {suc m} {suc _} m<n = cong suc (fromℕ<≡fromℕLessThan (ℕ.s<s⁻¹ m<n))
+fromℕ<≡fromℕLessThan = fromℕ<′≡fromℕLessThan
 
 fromℕ<-toℕ : (i : Fin n) .(i<n : toℕ i ℕ.< n) → fromℕ< i<n ≡ i
-fromℕ<-toℕ zero    _   = refl
-fromℕ<-toℕ (suc i) i<n = cong suc (fromℕ<-toℕ i (ℕ.s<s⁻¹ i<n))
-
-toℕ-fromℕ< : ∀ {m n} .(m<n : m ℕ.< n) → toℕ (fromℕ< m<n) ≡ m
-toℕ-fromℕ< {zero}  {suc _} _   = refl
-toℕ-fromℕ< {suc m} {suc n} m<n = cong suc (toℕ-fromℕ< (ℕ.s<s⁻¹ m<n))
-
-fromℕ<′-toℕ : (i : Fin n) → let instance _ = toℕ<n i in fromℕ<′ (toℕ i) ≡ i
-fromℕ<′-toℕ zero    = refl
-fromℕ<′-toℕ (suc i) = cong suc (fromℕ<′-toℕ i)
+fromℕ<-toℕ i i<n = begin
+  fromℕ< i<n
+    ≡⟨ fromℕ<≡fromℕLessThan ⦃ i<n ⦄ ⟩
+  fromℕLessThan (toℕ i)
+    ≡⟨ fromℕLessThan-toℕ i ⟩
+  i ∎ where open ≡-Reasoning ; instance _ = toℕ-LessThan i
+
+toℕ-fromℕ< : .(m<n : m ℕ.< n) → toℕ (fromℕ< m<n) ≡ m
+toℕ-fromℕ< {m = m} m<n = begin
+  toℕ (fromℕ< m<n)
+    ≡⟨ cong toℕ (fromℕ<≡fromℕLessThan ⦃ m<n ⦄) ⟩
+  toℕ (fromℕLessThan m)
+    ≡⟨ toℕ-fromℕLessThan m ⟩
+  m ∎ where open ≡-Reasoning; instance _ = ℕ.<-lessThan m<n
+
+fromℕ<-cong : ∀ m n {o} → m ≡ n → .(m<o : m ℕ.< o) .(n<o : n ℕ.< o) →
+              fromℕ< m<o ≡ fromℕ< n<o
+fromℕ<-cong m n r m<o n<o = fromℕ<′-cong {m} {n} ⦃ m<o ⦄ ⦃ n<o ⦄ r
 
-toℕ-fromℕ<′ : ∀ m {n} .{{_ : m ℕ.< n}} → toℕ (fromℕ<′ m) ≡ m
-toℕ-fromℕ<′ zero    {suc _} = refl
-toℕ-fromℕ<′ (suc m) {suc n} {{lt}} = cong suc (toℕ-fromℕ<′ m {n} {{ℕ.s<s⁻¹ lt}})
+fromℕ<-injective : ∀ m n {o} (m<o : m ℕ.< o) (n<o : n ℕ.< o) →
+                   fromℕ< m<o ≡ fromℕ< n<o →
+                   m ≡ n
+fromℕ<-injective m n m<o n<o = fromℕ<′-injective ⦃ m<o ⦄ ⦃ n<o ⦄
 
 -- fromℕ is a special case of fromℕ<.
 fromℕ-def : ∀ n → fromℕ n ≡ fromℕ< (ℕₚ.n<1+n n)
 fromℕ-def zero    = refl
 fromℕ-def (suc n) = cong suc (fromℕ-def n)
 
-fromℕ<-cong : ∀ m n {o} → m ≡ n → (m<o : m ℕ.< o) (n<o : n ℕ.< o) →
-              fromℕ< m<o ≡ fromℕ< n<o
-fromℕ<-cong 0       0               r _ _ = refl
-fromℕ<-cong (suc m) (suc n) {suc o} r m<o n<o
-  = cong suc (fromℕ<-cong m n (ℕₚ.suc-injective r) (s<s⁻¹ m<o) (s<s⁻¹ n<o))
-
-fromℕ<-injective : ∀ m n {o} → (m<o : m ℕ.< o) (n<o : n ℕ.< o) →
-                   fromℕ< m<o ≡ fromℕ< n<o →
-                   m ≡ n
-fromℕ<-injective 0       0       z<s       z<s       r = refl
-fromℕ<-injective (suc m) (suc n) (s<s m<o) (s<s n<o) r
-  = cong suc (fromℕ<-injective m n m<o n<o (suc-injective r))
-
 ------------------------------------------------------------------------
 -- fromℕ<″
 ------------------------------------------------------------------------
 
+fromℕ<″≡fromℕ : ∀ (m<″n : m ℕ.<″ n) →
+                let ℕ.less-than-or-equal {k} proof = m<″n
+                    instance _ = subst (ℕ.LessThan m) proof (ℕ.<″-lessThan {m} {k})
+                in
+                fromℕ<″ m m<″n ≡ fromℕLessThan m
+fromℕ<″≡fromℕ {m = zero}              (ℕ.<″-offset _) = refl
+fromℕ<″≡fromℕ {m = suc m} {n = suc n} (ℕ.<″-offset k) =
+  cong suc (fromℕ<″≡fromℕ (ℕ.<″-offset k))
+
+fromℕ<″≡fromℕ< : ∀ (m<″n : m ℕ.<″ n) →
+                 fromℕ<″ m m<″n ≡ fromℕ< (ℕₚ.≤″⇒≤ m<″n)
+fromℕ<″≡fromℕ< m<″n = fromℕ<″≡fromℕ m<″n
+
 fromℕ<≡fromℕ<″ : ∀ (m<n : m ℕ.< n) (m<″n : m ℕ.<″ n) →
                  fromℕ< m<n ≡ fromℕ<″ m m<″n
-fromℕ<≡fromℕ<″ z<s               (ℕ.<″-offset _) = refl
-fromℕ<≡fromℕ<″ (s<s m<n@(s≤s _)) (ℕ.<″-offset k) =
-  cong suc (fromℕ<≡fromℕ<″ m<n (ℕ.<″-offset k))
+fromℕ<≡fromℕ<″ _ m<″n = sym (fromℕ<″≡fromℕ< m<″n)
 
 toℕ-fromℕ<″ : ∀ (m<″n : m ℕ.<″ n) → toℕ (fromℕ<″ m m<″n) ≡ m
 toℕ-fromℕ<″ {m} {n} m<″n = begin
-  toℕ (fromℕ<″ m m<″n) ≡˘⟨ cong toℕ (fromℕ<≡fromℕ<″ m<n m<″n) ⟩
-  toℕ (fromℕ<  m<n)    ≡⟨ toℕ-fromℕ< m<n ⟩
-  m                    ∎
-  where open ≡-Reasoning ; m<n = ℕₚ.≤″⇒≤ m<″n
+  toℕ (fromℕ<″ m m<″n)        ≡⟨ cong toℕ (fromℕ<″≡fromℕ m<″n) ⟩
+  toℕ (fromℕLessThan m ⦃ _ ⦄) ≡⟨ toℕ-fromℕLessThan m ⦃ _ ⦄ ⟩
+  m                           ∎
+  where open ≡-Reasoning ; instance _ = ℕ.<-lessThan (ℕₚ.≤″⇒≤ m<″n)
 
 ------------------------------------------------------------------------
 -- Properties of cast
@@ -629,10 +685,10 @@ join-splitAt (suc m) n (suc i) = begin
 
 -- splitAt "m" "i" ≡ inj₁ "i" if i < m
 
-splitAt-LessThan : ∀ m {n} (i : Fin (m ℕ.+ n)) .{{_ : ℕ.LessThan (toℕ i) m}} →
-            splitAt m i ≡ inj₁ (fromℕLessThan (toℕ i))
-splitAt-LessThan (suc m) zero    = refl
-splitAt-LessThan (suc m) (suc i) = cong (Sum.map suc id) (splitAt-LessThan m i)
+splitAt-LessThan : ∀ m {n} (i : Fin (m ℕ.+ n)) .{{lt : ℕ.LessThan (toℕ i) m}} →
+            splitAt m i ≡ inj₁ (fromℕLessThan (toℕ i) ⦃ lt ⦄ )
+splitAt-LessThan (suc m) zero           = refl
+splitAt-LessThan (suc m) (suc i) ⦃ lt ⦄ = cong (Sum.map suc id) (splitAt-LessThan m i ⦃ lt ⦄)
 
 splitAt-< : ∀ m {n} (i : Fin (m ℕ.+ n)) .(i<m : toℕ i ℕ.< m) →
             splitAt m i ≡ inj₁ (fromℕ< i<m)

From c1c13d5c54633a075c16813ee587a27dc0340b2d Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 24 Jun 2023 15:27:56 +0100
Subject: [PATCH 24/80] streamlined type signatures

---
 src/Data/Fin/Properties.agda | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 7da1e082f4..f795e85a2e 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -222,13 +222,13 @@ toℕ-fromℕLessThan : ∀ m {n} .⦃ _ : ℕ.LessThan m n ⦄ → toℕ (from
 toℕ-fromℕLessThan zero    {suc _} = refl
 toℕ-fromℕLessThan (suc m) {suc _} = cong suc (toℕ-fromℕLessThan m)
 
-fromℕLessThan-cong : ∀ {m n o} ⦃ m<o : ℕ.LessThan m o ⦄ ⦃ n<o : ℕ.LessThan n o ⦄ →
-                     m ≡ n → fromℕLessThan m {o} ⦃ m<o ⦄ ≡ fromℕLessThan n {o} ⦃ n<o ⦄
+fromℕLessThan-cong : ∀ {m n o} ⦃ m<o : _ ⦄ ⦃ n<o : _ ⦄ → m ≡ n →
+                     fromℕLessThan m {o} ⦃ m<o ⦄ ≡ fromℕLessThan n {o} ⦃ n<o ⦄
 fromℕLessThan-cong {zero}  {zero}                          r = refl
 fromℕLessThan-cong {suc m} {suc n} {suc _} ⦃ m<o ⦄ ⦃ n<o ⦄ r
   = cong suc (fromℕLessThan-cong {m} {n} ⦃ m<o ⦄ ⦃ n<o ⦄ (ℕₚ.suc-injective r))
 
-fromℕLessThan-injective : ∀ {m n o} ⦃ m<o : ℕ.LessThan m o ⦄ ⦃ n<o : ℕ.LessThan n o ⦄ →
+fromℕLessThan-injective : ∀ {m n o} ⦃ m<o : _ ⦄ ⦃ n<o : _ ⦄ →
                           fromℕLessThan m {o} ⦃ m<o ⦄ ≡ fromℕLessThan n {o} ⦃ n<o ⦄ →
                           m ≡ n
 fromℕLessThan-injective {zero}  {zero}          r = refl
@@ -337,7 +337,7 @@ toℕ-fromℕ<″ {m} {n} m<″n = begin
   toℕ (fromℕ<″ m m<″n)        ≡⟨ cong toℕ (fromℕ<″≡fromℕ m<″n) ⟩
   toℕ (fromℕLessThan m ⦃ _ ⦄) ≡⟨ toℕ-fromℕLessThan m ⦃ _ ⦄ ⟩
   m                           ∎
-  where open ≡-Reasoning ; instance _ = ℕ.<-lessThan (ℕₚ.≤″⇒≤ m<″n)
+  where open ≡-Reasoning
 
 ------------------------------------------------------------------------
 -- Properties of cast
@@ -685,10 +685,11 @@ join-splitAt (suc m) n (suc i) = begin
 
 -- splitAt "m" "i" ≡ inj₁ "i" if i < m
 
-splitAt-LessThan : ∀ m {n} (i : Fin (m ℕ.+ n)) .{{lt : ℕ.LessThan (toℕ i) m}} →
-            splitAt m i ≡ inj₁ (fromℕLessThan (toℕ i) ⦃ lt ⦄ )
+splitAt-LessThan : ∀ m {n} (i : Fin (m ℕ.+ n)) .⦃ lt : _ ⦄ →
+                   splitAt m i ≡ inj₁ (fromℕLessThan (toℕ i) ⦃ lt ⦄ )
 splitAt-LessThan (suc m) zero           = refl
-splitAt-LessThan (suc m) (suc i) ⦃ lt ⦄ = cong (Sum.map suc id) (splitAt-LessThan m i ⦃ lt ⦄)
+splitAt-LessThan (suc m) (suc i) ⦃ lt ⦄ =
+  cong (Sum.map suc id) (splitAt-LessThan m i ⦃ lt ⦄)
 
 splitAt-< : ∀ m {n} (i : Fin (m ℕ.+ n)) .(i<m : toℕ i ℕ.< m) →
             splitAt m i ≡ inj₁ (fromℕ< i<m)

From 1bff854745f57e97a95be7f38632ba624dfa5082 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 24 Jun 2023 18:40:55 +0100
Subject: [PATCH 25/80] towards deprecation; lightneend dependencies

---
 src/Data/List/Relation/Unary/Linked/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/List/Relation/Unary/Linked/Properties.agda b/src/Data/List/Relation/Unary/Linked/Properties.agda
index 7106ad3e1e..5c3fc896c7 100644
--- a/src/Data/List/Relation/Unary/Linked/Properties.agda
+++ b/src/Data/List/Relation/Unary/Linked/Properties.agda
@@ -17,7 +17,7 @@ open import Data.List.Relation.Unary.All using (All; []; _∷_)
 open import Data.List.Relation.Unary.Linked as Linked
   using (Linked; []; [-]; _∷_)
 open import Data.Nat.Base using (zero; suc; _<_; z<s; s<s)
-open import Data.Nat.Properties using (≤-refl; ≤-pred; m≤n⇒m≤1+n)
+open import Data.Nat.Properties using (≤-refl; m≤n⇒m≤1+n)
 open import Data.Maybe.Relation.Binary.Connected
   using (Connected; just; nothing; just-nothing; nothing-just)
 open import Level using (Level)

From cc7ef6d48e32750f5be3fe4530bf1de5f393fc10 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 24 Jun 2023 18:44:13 +0100
Subject: [PATCH 26/80] towards deprecation

---
 src/Data/Vec/Bounded/Base.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/Vec/Bounded/Base.agda b/src/Data/Vec/Bounded/Base.agda
index 9c874ec89e..f76301e96b 100644
--- a/src/Data/Vec/Bounded/Base.agda
+++ b/src/Data/Vec/Bounded/Base.agda
@@ -132,12 +132,12 @@ align = alignWith id
 take : ∀ {m} n → Vec≤ A m → Vec≤ A (n ⊓ m)
 take             zero    _                = []
 take             (suc n) (Vec.[] , p)     = []
-take {m = suc m} (suc n) (a Vec.∷ as , p) = a ∷ take n (as , ℕₚ.≤-pred p)
+take {m = suc m} (suc n) (a Vec.∷ as , p) = a ∷ take n (as , s≤s⁻¹ p)
 
 drop : ∀ {m} n → Vec≤ A m → Vec≤ A (m ∸ n)
 drop             zero    v                = v
 drop             (suc n) (Vec.[] , p)     = []
-drop {m = suc m} (suc n) (a Vec.∷ as , p) = drop n (as , ℕₚ.≤-pred p)
+drop {m = suc m} (suc n) (a Vec.∷ as , p) = drop n (as , s≤s⁻¹ p)
 
 ------------------------------------------------------------------------
 -- Lifting a collection of bounded vectors to the same size

From f4f6ef0790eec6228909ecc9741a789906f758e2 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 24 Jun 2023 18:49:49 +0100
Subject: [PATCH 27/80] towards deprecation

---
 src/Data/Nat/Binary/Properties.agda | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda
index 3ea094ec00..fcc68fa0e2 100644
--- a/src/Data/Nat/Binary/Properties.agda
+++ b/src/Data/Nat/Binary/Properties.agda
@@ -15,7 +15,7 @@ open import Algebra.Consequences.Propositional
 open import Data.Bool.Base using (if_then_else_; Bool; true; false)
 open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Data.Nat.Binary.Base
-open import Data.Nat as ℕ using (ℕ; z≤n; s≤s)
+open import Data.Nat as ℕ using (ℕ; z≤n; s≤s; s<s⁻¹)
 open import Data.Nat.DivMod using (_%_; _/_; m/n≤m; +-distrib-/-∣ˡ)
 open import Data.Nat.Divisibility using (∣-refl)
 import Data.Nat.Base as ℕᵇ
@@ -303,17 +303,17 @@ toℕ-cancel-< : ∀ {x y} → toℕ x ℕ.< toℕ y → x < y
 toℕ-cancel-< {zero}     {2[1+ y ]} x<y = 0<even
 toℕ-cancel-< {zero}     {1+[2 y ]} x<y = 0<odd
 toℕ-cancel-< {2[1+ x ]} {2[1+ y ]} x<y =
-  even<even (toℕ-cancel-< (ℕ.≤-pred (ℕₚ.*-cancelˡ-< 2 _ _ x<y)))
+  even<even (toℕ-cancel-< (s<s⁻¹ (ℕₚ.*-cancelˡ-< 2 _ _ x<y)))
 toℕ-cancel-< {2[1+ x ]} {1+[2 y ]} x<y
   rewrite ℕₚ.*-distribˡ-+ 2 1 (toℕ x) =
-  even<odd (toℕ-cancel-< (ℕₚ.*-cancelˡ-< 2 _ _ (ℕₚ.≤-trans (s≤s (ℕₚ.n≤1+n _)) (ℕₚ.≤-pred x<y))))
+  even<odd (toℕ-cancel-< (ℕₚ.*-cancelˡ-< 2 _ _ (ℕₚ.≤-trans (s≤s (ℕₚ.n≤1+n _)) (s<s⁻¹ x<y))))
 toℕ-cancel-< {1+[2 x ]} {2[1+ y ]} x<y with toℕ x ℕₚ.≟ toℕ y
 ... | yes x≡y = odd<even (inj₂ (toℕ-injective x≡y))
 ... | no  x≢y
   rewrite ℕₚ.+-suc (toℕ y) (toℕ y ℕ.+ 0) =
   odd<even (inj₁ (toℕ-cancel-< (ℕₚ.≤∧≢⇒< (ℕₚ.*-cancelˡ-≤ 2 (ℕₚ.+-cancelˡ-≤ 2 _ _ x<y)) x≢y)))
 toℕ-cancel-< {1+[2 x ]} {1+[2 y ]} x<y =
-  odd<odd (toℕ-cancel-< (ℕₚ.*-cancelˡ-< 2 _ _ (ℕ.≤-pred x<y)))
+  odd<odd (toℕ-cancel-< (ℕₚ.*-cancelˡ-< 2 _ _ (s<s⁻¹ x<y)))
 
 fromℕ-cancel-< : ∀ {x y} → fromℕ x < fromℕ y → x ℕ.< y
 fromℕ-cancel-< = subst₂ ℕ._<_ (toℕ-fromℕ _) (toℕ-fromℕ _) ∘ toℕ-mono-<

From 24fe5a0ef6c2d71e026828e2ca744a4103ef089e Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 24 Jun 2023 20:41:40 +0100
Subject: [PATCH 28/80] towards deprecation

---
 src/Data/Integer/Properties.agda | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda
index 518c1456f4..a35d25d013 100644
--- a/src/Data/Integer/Properties.agda
+++ b/src/Data/Integer/Properties.agda
@@ -17,7 +17,7 @@ import Algebra.Properties.AbelianGroup
 open import Data.Bool.Base using (T; true; false)
 open import Data.Integer.Base renaming (suc to sucℤ)
 open import Data.Nat as ℕ
-  using (ℕ; suc; zero; _∸_; s≤s; z≤n; s<s; z<s)
+  using (ℕ; suc; zero; _∸_; s≤s; z≤n; s<s; z<s; s≤s⁻¹; s<s⁻¹)
   hiding (module ℕ)
 import Data.Nat.Properties as ℕ
 open import Data.Nat.Solver
@@ -297,9 +297,9 @@ drop‿-<- (-<- n<m) = n<m
 ... | tri≈ m≮n m≡n n≯m = tri≈ (n≯m ∘ drop‿-<-) (cong -[1+_] m≡n) (m≮n ∘ drop‿-<-)
 ... | tri> m≮n m≢n n>m = tri< (-<- n>m) (m≢n ∘ -[1+-injective) (m≮n ∘ drop‿-<-)
 <-cmp +[1+ m ] +[1+ n ] with ℕ.<-cmp m n
-... | tri< m<n m≢n n≯m = tri< (+<+ (s<s m<n))              (m≢n ∘ +[1+-injective) (n≯m ∘ ℕ.≤-pred ∘ drop‿+<+)
-... | tri≈ m≮n m≡n n≯m = tri≈ (m≮n ∘ ℕ.≤-pred ∘ drop‿+<+) (cong (+_ ∘ suc) m≡n)  (n≯m ∘ ℕ.≤-pred ∘ drop‿+<+)
-... | tri> m≮n m≢n n>m = tri> (m≮n ∘ ℕ.≤-pred ∘ drop‿+<+) (m≢n ∘ +[1+-injective) (+<+ (s<s n>m))
+... | tri< m<n m≢n n≯m = tri< (+<+ (s<s m<n))              (m≢n ∘ +[1+-injective) (n≯m ∘ s<s⁻¹ ∘ drop‿+<+)
+... | tri≈ m≮n m≡n n≯m = tri≈ (m≮n ∘ s<s⁻¹ ∘ drop‿+<+) (cong (+_ ∘ suc) m≡n)  (n≯m ∘ s<s⁻¹ ∘ drop‿+<+)
+... | tri> m≮n m≢n n>m = tri> (m≮n ∘ s<s⁻¹ ∘ drop‿+<+) (m≢n ∘ +[1+-injective) (+<+ (s<s n>m))
 
 infix 4 _<?_
 _<?_ : Decidable _<_
@@ -427,7 +427,7 @@ neg-mono-< { -[1+ _ ]} { -[1+ _ ]} (-<- n<m) = +<+ (s<s n<m)
 neg-mono-< { -[1+ _ ]} { +0}       -<+       = +<+ z<s
 neg-mono-< { -[1+ _ ]} { +[1+ n ]} -<+       = -<+
 neg-mono-< { +0}       { +[1+ n ]} (+<+ _)   = -<+
-neg-mono-< { +[1+ m ]} { +[1+ n ]} (+<+ m<n) = -<- (ℕ.≤-pred m<n)
+neg-mono-< { +[1+ m ]} { +[1+ n ]} (+<+ m<n) = -<- (s<s⁻¹ m<n)
 
 neg-cancel-< : - i < - j → i > j
 neg-cancel-< { +[1+ m ]} { +[1+ n ]} (-<- n<m)       = +<+ (s<s n<m)
@@ -436,7 +436,7 @@ neg-cancel-< { +[1+ m ]} { -[1+ n ]}  -<+            = -<+
 neg-cancel-< { +0}       { +0}       (+<+ ())
 neg-cancel-< { +0}       { -[1+ n ]} _               = -<+
 neg-cancel-< { -[1+ m ]} { +0}       (+<+ ())
-neg-cancel-< { -[1+ m ]} { -[1+ n ]} (+<+ (s<s m<n)) = -<- m<n
+neg-cancel-< { -[1+ m ]} { -[1+ n ]} (+<+ m<n) = -<- (s<s⁻¹ m<n)
 
 ------------------------------------------------------------------------
 -- Properties of ∣_∣
@@ -1227,12 +1227,12 @@ suc[i]≤j⇒i<j : sucℤ i ≤ j → i < j
 suc[i]≤j⇒i<j {+ i}           {+ _}       (+≤+ i≤j) = +<+ i≤j
 suc[i]≤j⇒i<j { -[1+ 0 ]}     {+ j}       p         = -<+
 suc[i]≤j⇒i<j { -[1+ suc i ]} {+ j}       -≤+       = -<+
-suc[i]≤j⇒i<j { -[1+ suc i ]} { -[1+ j ]} (-≤- j≤i) = -<- (ℕ.s≤s j≤i)
+suc[i]≤j⇒i<j { -[1+ suc i ]} { -[1+ j ]} (-≤- j≤i) = -<- (s≤s j≤i)
 
 i<j⇒suc[i]≤j : i < j → sucℤ i ≤ j
 i<j⇒suc[i]≤j {+ _}           {+ _}       (+<+ i<j) = +≤+ i<j
 i<j⇒suc[i]≤j { -[1+ 0 ]}     {+ _}       -<+       = +≤+ z≤n
-i<j⇒suc[i]≤j { -[1+ suc i ]} { -[1+ _ ]} (-<- j<i) = -≤- (ℕ.≤-pred j<i)
+i<j⇒suc[i]≤j { -[1+ suc i ]} { -[1+ _ ]} (-<- j<i) = -≤- (s≤s⁻¹ j<i)
 i<j⇒suc[i]≤j { -[1+ suc i ]} {+ _}       -<+       = -≤+
 
 ------------------------------------------------------------------------
@@ -1282,7 +1282,7 @@ i≤pred[j]⇒i<j {_} { -[1+ n ]} leq = ≤-<-trans leq (-<- ℕ.≤-refl)
 i<j⇒i≤pred[j] : i < j → i ≤ pred j
 i<j⇒i≤pred[j] {_} { +0}       -<+       = -≤- z≤n
 i<j⇒i≤pred[j] {_} { +[1+ n ]} -<+       = -≤+
-i<j⇒i≤pred[j] {_} { +[1+ n ]} (+<+ m<n) = +≤+ (ℕ.≤-pred m<n)
+i<j⇒i≤pred[j] {_} { +[1+ n ]} (+<+ m<n) = +≤+ (s≤s⁻¹ m<n)
 i<j⇒i≤pred[j] {_} { -[1+ n ]} (-<- n<m) = -≤- n<m
 
 i≤j⇒pred[i]≤j : i ≤ j → pred i ≤ j
@@ -1717,7 +1717,7 @@ neg-distribʳ-* i j = begin
 
 *-cancelʳ-≤-pos : ∀ i j k .{{_ : Positive k}} → i * k ≤ j * k → i ≤ j
 *-cancelʳ-≤-pos -[1+ m ] -[1+ n ] +[1+ o ] (-≤- n≤m) =
-  -≤- (ℕ.≤-pred (ℕ.*-cancelʳ-≤ (suc n) (suc m) (suc o) (s≤s n≤m)))
+  -≤- (s≤s⁻¹ (ℕ.*-cancelʳ-≤ (suc n) (suc m) (suc o) (s≤s n≤m)))
 *-cancelʳ-≤-pos -[1+ _ ] (+ _)    +[1+ o ] _         = -≤+
 *-cancelʳ-≤-pos +0       +0       +[1+ o ] _         = +≤+ z≤n
 *-cancelʳ-≤-pos +0       +[1+ _ ] +[1+ o ] _         = +≤+ z≤n
@@ -1732,7 +1732,7 @@ neg-distribʳ-* i j = begin
 *-monoʳ-≤-nonNeg +0 {i} {j} i≤j rewrite *-zeroʳ i | *-zeroʳ j = +≤+ z≤n
 *-monoʳ-≤-nonNeg +[1+ n ] (-≤+ {n = 0})         = -≤+
 *-monoʳ-≤-nonNeg +[1+ n ] (-≤+ {n = suc _})     = -≤+
-*-monoʳ-≤-nonNeg +[1+ n ] (-≤- n≤m) = -≤- (ℕ.≤-pred (ℕ.*-mono-≤ (s≤s n≤m) (ℕ.≤-refl {x = suc n})))
+*-monoʳ-≤-nonNeg +[1+ n ] (-≤- n≤m) = -≤- (s≤s⁻¹ (ℕ.*-mono-≤ (s≤s n≤m) (ℕ.≤-refl {x = suc n})))
 *-monoʳ-≤-nonNeg +[1+ n ] {+0}       {+0}       (+≤+ m≤n) = +≤+ m≤n
 *-monoʳ-≤-nonNeg +[1+ n ] {+0}       {+[1+ _ ]} (+≤+ m≤n) = +≤+ z≤n
 *-monoʳ-≤-nonNeg +[1+ n ] {+[1+ _ ]} {+[1+ _ ]} (+≤+ m≤n) = +≤+ (ℕ.*-monoˡ-≤ (suc n) m≤n)
@@ -1782,7 +1782,7 @@ neg-distribʳ-* i j = begin
 *-cancelˡ-<-nonNeg {+ i}       {+ j}       (+ n) leq = +<+ (ℕ.*-cancelˡ-< n _ _ (+◃-cancel-< leq))
 *-cancelˡ-<-nonNeg {+ i}       { -[1+ j ]} (+ n) leq = contradiction leq +◃≮-◃
 *-cancelˡ-<-nonNeg { -[1+ i ]} {+ j}       (+ n)leq = -<+
-*-cancelˡ-<-nonNeg { -[1+ i ]} { -[1+ j ]} (+ n) leq = -<- (ℕ.≤-pred (ℕ.*-cancelˡ-< n _ _ (neg◃-cancel-< leq)))
+*-cancelˡ-<-nonNeg { -[1+ i ]} { -[1+ j ]} (+ n) leq = -<- (s<s⁻¹ (ℕ.*-cancelˡ-< n _ _ (neg◃-cancel-< leq)))
 
 *-cancelʳ-<-nonNeg : ∀ k .{{_ : NonNegative k}} → i * k < j * k → i < j
 *-cancelʳ-<-nonNeg {i} {j} k rewrite *-comm i k | *-comm j k = *-cancelˡ-<-nonNeg k

From ef0c01cb6cd9df7eea3988ae68adcb8af083d427 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 24 Jun 2023 20:42:26 +0100
Subject: [PATCH 29/80] Nathan's `LessThan` instance

---
 src/Data/Nat/Base.agda | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda
index 9b960da60f..83a13bcdcf 100644
--- a/src/Data/Nat/Base.agda
+++ b/src/Data/Nat/Base.agda
@@ -262,6 +262,13 @@ lessThanSuc : ∀ {n} → LessThan n (suc n)
 lessThanSuc {zero}  = _
 lessThanSuc {suc n} = lessThanSuc {n}
 
+lessThanSucSuc : ∀ {m n} → ⦃ LessThan m n ⦄ → LessThan (suc m) (suc n)
+lessThanSucSuc ⦃ lt ⦄ = lt
+{-
+lessThanSucSuc {zero}  {suc _} = _
+lessThanSucSuc {suc m} {suc n} = lessThanSucSuc {m} {n}
+-}
+
 <-lessThan : ∀ {m n} → .(m<n : m < n) → LessThan m n
 <-lessThan {zero}  {suc n}       = _
 <-lessThan {suc m} {suc n} (m<n) = <-lessThan {m} {n} (s<s⁻¹ m<n)

From 014a665cfbcf440bee535cf4fcae7af2b4b780b2 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 25 Jun 2023 06:09:11 +0100
Subject: [PATCH 30/80] =?UTF-8?q?DEPRECATIONS=20plus=20redefinitions=20of?=
 =?UTF-8?q?=20`=E2=89=A4-pred`=20`<-pred`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Data/Nat.agda            | 11 ++++++++++-
 src/Data/Nat/Properties.agda | 16 +++++++++++-----
 2 files changed, 21 insertions(+), 6 deletions(-)

diff --git a/src/Data/Nat.agda b/src/Data/Nat.agda
index 1abd7d9d7c..1a4f06b475 100644
--- a/src/Data/Nat.agda
+++ b/src/Data/Nat.agda
@@ -42,5 +42,14 @@ open import Data.Nat.Properties public
 
 -- Version 0.17
 
+-- Version 2.0
+
 open import Data.Nat.Properties public
-  using (≤-pred)
+  hiding (≤-pred; <-pred)
+
+≤-pred : ∀ {m n} → (m ≤ n) → pred m ≤ pred n
+≤-pred {m = zero}              _   = z≤n
+≤-pred {m = suc _} {n = suc _} m≤n = s≤s⁻¹ m≤n
+
+<-pred : ∀ {m n} → .⦃ _ : NonZero m ⦄ → (m < n) → pred m < pred n
+<-pred {m = suc _} {n = suc _} = s<s⁻¹
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index feac800985..5922045c3a 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -155,8 +155,6 @@ lessThan? (suc m) (suc n) = lessThan? m n
 ≤-reflexive {zero}  refl = z≤n
 ≤-reflexive {suc m} refl = s≤s (≤-reflexive refl)
 
-≤-pred = s≤s⁻¹
-
 ≤-refl : Reflexive _≤_
 ≤-refl = ≤-reflexive refl
 
@@ -419,8 +417,6 @@ _>?_ = flip _<?_
 s<s-injective : ∀ {m n} {p q : m < n} → s<s p ≡ s<s q → p ≡ q
 s<s-injective refl = refl
 
-<-pred = s<s⁻¹
-
 m<n⇒m<1+n : ∀ {m n} → m < n → m < 1 + n
 m<n⇒m<1+n z<s               = z<s
 m<n⇒m<1+n (s<s m<n@(s≤s _)) = s<s (m<n⇒m<1+n m<n)
@@ -707,7 +703,7 @@ m+n≤o⇒n≤o (suc m) m+n<o = m+n≤o⇒n≤o m (<⇒≤ m+n<o)
 +-monoʳ-< (suc n) m≤o = s≤s (+-monoʳ-< n m≤o)
 
 m+1+n≰m : ∀ m {n} → m + suc n ≰ m
-m+1+n≰m (suc m) (s≤s m+1+n≤m) = m+1+n≰m m m+1+n≤m
+m+1+n≰m (suc m) m+1+n≤m = m+1+n≰m m (s≤s⁻¹ m+1+n≤m)
 
 m<m+n : ∀ m {n} → n > 0 → m < m + n
 m<m+n zero    n>0 = n>0
@@ -2298,6 +2294,16 @@ suc[pred[n]]≡n {suc n} _   = refl
 "Warning: suc[pred[n]]≡n was deprecated in v2.0. Please use suc-pred instead. Note that the proof now uses instance arguments"
 #-}
 
+≤-pred = s≤s⁻¹
+{-# WARNING_ON_USAGE ≤-pred
+"Warning: ≤-pred was deprecated in v2.0. Please use Data.Nat.Base.s≤s⁻¹  or Data.Nat.≤-pred instead. Note that the latter now has a different type. "
+#-}
+
+<-pred = s<s⁻¹
+{-# WARNING_ON_USAGE ≤-pred
+"Warning: <-pred was deprecated in v2.0. Please use Data.Nat.Base.s<s⁻¹ or Data.Nat.<-pred instead. Note that the latter now has a different type using instance arguments."
+#-}
+
 ≤-step = m≤n⇒m≤1+n
 {-# WARNING_ON_USAGE ≤-step
 "Warning: ≤-step was deprecated in v2.0. Please use m≤n⇒m≤1+n instead. "

From 2f2252a36f06ea1f5b785d0934266593eb66140e Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 25 Jun 2023 06:26:10 +0100
Subject: [PATCH 31/80] tidied up som e irrefutable `with` patterns

---
 src/Data/Fin/Properties.agda | 28 ++++++++++++++++------------
 1 file changed, 16 insertions(+), 12 deletions(-)

diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index f795e85a2e..0bc83ebfd5 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -657,8 +657,10 @@ splitAt-↑ˡ (suc m) (suc i) n rewrite splitAt-↑ˡ m i n = refl
 
 splitAt⁻¹-↑ˡ : ∀ {m} {n} {i} {j} → splitAt m {n} i ≡ inj₁ j → j ↑ˡ n ≡ i
 splitAt⁻¹-↑ˡ {suc m} {n} {0F} {.0F} refl = refl
-splitAt⁻¹-↑ˡ {suc m} {n} {suc i} {j} eq with splitAt m i in splitAt[m][i]≡inj₁[j]
-... | inj₁ k with refl ← eq = cong suc (splitAt⁻¹-↑ˡ {i = i} {j = k} splitAt[m][i]≡inj₁[j])
+splitAt⁻¹-↑ˡ {suc m} {n} {suc i} {j} eq
+  with inj₁ k ← splitAt m i in splitAt[m][i]≡inj₁[j]
+  with refl ← eq
+  = cong suc (splitAt⁻¹-↑ˡ {i = i} {j = k} splitAt[m][i]≡inj₁[j])
 
 splitAt-↑ʳ : ∀ m n i → splitAt m (m ↑ʳ i) ≡ inj₂ {B = Fin n} i
 splitAt-↑ʳ zero    n i = refl
@@ -666,8 +668,10 @@ splitAt-↑ʳ (suc m) n i rewrite splitAt-↑ʳ m n i = refl
 
 splitAt⁻¹-↑ʳ : ∀ {m} {n} {i} {j} → splitAt m {n} i ≡ inj₂ j → m ↑ʳ j ≡ i
 splitAt⁻¹-↑ʳ {zero}  {n} {i} {j} refl = refl
-splitAt⁻¹-↑ʳ {suc m} {n} {suc i} {j} eq with splitAt m i in splitAt[m][i]≡inj₂[k]
-... | inj₂ k with refl ← eq = cong suc (splitAt⁻¹-↑ʳ {i = i} {j = k} splitAt[m][i]≡inj₂[k])
+splitAt⁻¹-↑ʳ {suc m} {n} {suc i} {j} eq
+  with inj₂ k ← splitAt m i in splitAt[m][i]≡inj₂[k]
+  with refl ← eq
+  = cong suc (splitAt⁻¹-↑ʳ {i = i} {j = k} splitAt[m][i]≡inj₂[k])
 
 splitAt-join : ∀ m n i → splitAt m (join m n i) ≡ i
 splitAt-join m n (inj₁ x) = splitAt-↑ˡ m x n
@@ -772,8 +776,9 @@ combine-injectiveˡ i j k l cᵢⱼ≡cₖₗ with <-cmp i k
 
 combine-injectiveʳ : ∀ (i : Fin m) (j : Fin n) (k : Fin m) (l : Fin n) →
                      combine i j ≡ combine k l → j ≡ l
-combine-injectiveʳ {m} {n} i j k l cᵢⱼ≡cₖₗ with combine-injectiveˡ i j k l cᵢⱼ≡cₖₗ
-... | refl = toℕ-injective (ℕₚ.+-cancelˡ-≡ (n ℕ.* toℕ i) _ _ (begin
+combine-injectiveʳ {m} {n} i j k l cᵢⱼ≡cₖₗ
+  with refl ← combine-injectiveˡ i j k l cᵢⱼ≡cₖₗ
+  = toℕ-injective (ℕₚ.+-cancelˡ-≡ (n ℕ.* toℕ i) _ _ (begin
   n ℕ.* toℕ i ℕ.+ toℕ j ≡˘⟨ toℕ-combine i j ⟩
   toℕ (combine i j)     ≡⟨ cong toℕ cᵢⱼ≡cₖₗ ⟩
   toℕ (combine i l)     ≡⟨ toℕ-combine i l ⟩
@@ -787,8 +792,8 @@ combine-injective i j k l cᵢⱼ≡cₖₗ =
   combine-injectiveʳ i j k l cᵢⱼ≡cₖₗ
 
 combine-surjective : ∀ (i : Fin (m ℕ.* n)) → ∃₂ λ j k → combine j k ≡ i
-combine-surjective {m} {n} i with remQuot {m} n i in eq
-... | j , k = j , k , (begin
+combine-surjective {m} {n} i with j , k ← remQuot {m} n i in eq
+  = j , k , (begin
   combine j k                       ≡˘⟨ uncurry (cong₂ combine) (,-injective eq) ⟩
   uncurry combine (remQuot {m} n i) ≡⟨ combine-remQuot {m} n i ⟩
   i                                 ∎)
@@ -1075,10 +1080,9 @@ pigeonhole : m ℕ.< n → (f : Fin n → Fin m) → ∃₂ λ i j → i < j ×
 pigeonhole z<s               f = contradiction (f zero) λ()
 pigeonhole (s<s m<n@(s≤s _)) f with any? (λ k → f zero ≟ f (suc k))
 ... | yes (j , f₀≡fⱼ) = zero , suc j , z<s , f₀≡fⱼ
-... | no  f₀≢fₖ with pigeonhole m<n (λ j → punchOut (f₀≢fₖ ∘ (j ,_ )))
-...   | (i , j , i<j , fᵢ≡fⱼ) =
-  suc i , suc j , s<s i<j ,
-  punchOut-injective (f₀≢fₖ ∘ (i ,_)) _ fᵢ≡fⱼ
+... | no  f₀≢fₖ
+  with i , j , i<j , fᵢ≡fⱼ ← pigeonhole m<n (λ j → punchOut (f₀≢fₖ ∘ (j ,_ )))
+  = suc i , suc j , s<s i<j , punchOut-injective (f₀≢fₖ ∘ (i ,_)) _ fᵢ≡fⱼ
 
 injective⇒≤ : ∀ {f : Fin m → Fin n} → Injective _≡_ _≡_ f → m ℕ.≤ n
 injective⇒≤ {zero}  {_}     {f} _   = z≤n

From e7d75d3007a78887f088740e4b6a5c0397b7d143 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 28 Jun 2023 09:00:02 +0100
Subject: [PATCH 32/80] simplification via instance `lessThanSucSuc`

---
 src/Data/Fin/Properties.agda | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 0bc83ebfd5..9980c736e6 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -692,8 +692,9 @@ join-splitAt (suc m) n (suc i) = begin
 splitAt-LessThan : ∀ m {n} (i : Fin (m ℕ.+ n)) .⦃ lt : _ ⦄ →
                    splitAt m i ≡ inj₁ (fromℕLessThan (toℕ i) ⦃ lt ⦄ )
 splitAt-LessThan (suc m) zero           = refl
-splitAt-LessThan (suc m) (suc i) ⦃ lt ⦄ =
-  cong (Sum.map suc id) (splitAt-LessThan m i ⦃ lt ⦄)
+splitAt-LessThan (suc m) (suc i) =
+  cong (Sum.map suc id) (splitAt-LessThan m i)
+  where instance _ = ℕ.lessThanSucSuc
 
 splitAt-< : ∀ m {n} (i : Fin (m ℕ.+ n)) .(i<m : toℕ i ℕ.< m) →
             splitAt m i ≡ inj₁ (fromℕ< i<m)

From 3894b5997c8ffbb3c683b22a1a882ef98807bc55 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 28 Jun 2023 09:15:25 +0100
Subject: [PATCH 33/80] further simplification

---
 src/Data/Fin/Properties.agda | 12 ++++++------
 src/Data/Nat/Base.agda       |  4 ++--
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 9980c736e6..9c14dd4483 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -224,17 +224,17 @@ toℕ-fromℕLessThan (suc m) {suc _} = cong suc (toℕ-fromℕLessThan m)
 
 fromℕLessThan-cong : ∀ {m n o} ⦃ m<o : _ ⦄ ⦃ n<o : _ ⦄ → m ≡ n →
                      fromℕLessThan m {o} ⦃ m<o ⦄ ≡ fromℕLessThan n {o} ⦃ n<o ⦄
-fromℕLessThan-cong {zero}  {zero}                          r = refl
-fromℕLessThan-cong {suc m} {suc n} {suc _} ⦃ m<o ⦄ ⦃ n<o ⦄ r
-  = cong suc (fromℕLessThan-cong {m} {n} ⦃ m<o ⦄ ⦃ n<o ⦄ (ℕₚ.suc-injective r))
+fromℕLessThan-cong {zero}  {zero}          r = refl
+fromℕLessThan-cong {suc m} {suc n} {suc _} r
+  = cong suc (fromℕLessThan-cong {m} {n} (ℕₚ.suc-injective r))
 
 fromℕLessThan-injective : ∀ {m n o} ⦃ m<o : _ ⦄ ⦃ n<o : _ ⦄ →
                           fromℕLessThan m {o} ⦃ m<o ⦄ ≡ fromℕLessThan n {o} ⦃ n<o ⦄ →
                           m ≡ n
 fromℕLessThan-injective {zero}  {zero}          r = refl
-fromℕLessThan-injective {zero}  {suc n} {suc _} ()
-fromℕLessThan-injective {suc m} {suc n} {suc _} ⦃ m<o ⦄ ⦃ n<o ⦄ r
-  = cong suc (fromℕLessThan-injective {m} {n} ⦃ m<o ⦄ ⦃ n<o ⦄ (suc-injective r))
+fromℕLessThan-injective {zero}  {suc n} {suc _} () -- unexpectedly necessary?
+fromℕLessThan-injective {suc m} {suc n} {suc _} r
+  = cong suc (fromℕLessThan-injective {m} {n} (suc-injective r))
 
 -- fromℕ is a special case of fromℕLessThan.
 fromℕ-LessThan-def : ∀ n → let instance _ = ℕ.lessThanSuc {n} in
diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda
index 83a13bcdcf..43faae290e 100644
--- a/src/Data/Nat/Base.agda
+++ b/src/Data/Nat/Base.agda
@@ -263,11 +263,11 @@ lessThanSuc {zero}  = _
 lessThanSuc {suc n} = lessThanSuc {n}
 
 lessThanSucSuc : ∀ {m n} → ⦃ LessThan m n ⦄ → LessThan (suc m) (suc n)
-lessThanSucSuc ⦃ lt ⦄ = lt
 {-
+lessThanSucSuc ⦃ lt ⦄ = lt
+-}
 lessThanSucSuc {zero}  {suc _} = _
 lessThanSucSuc {suc m} {suc n} = lessThanSucSuc {m} {n}
--}
 
 <-lessThan : ∀ {m n} → .(m<n : m < n) → LessThan m n
 <-lessThan {zero}  {suc n}       = _

From 1c30be6d2c5ccc50468be9402934dd8f2c19dd5e Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 29 Jun 2023 09:34:08 +0100
Subject: [PATCH 34/80] simplified dependencies

---
 src/Data/Nat/Show/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Nat/Show/Properties.agda b/src/Data/Nat/Show/Properties.agda
index 393b9c9fe1..fa120642cb 100644
--- a/src/Data/Nat/Show/Properties.agda
+++ b/src/Data/Nat/Show/Properties.agda
@@ -8,7 +8,7 @@
 
 open import Data.Digit using (showDigit; toDigits)
 open import Data.Digit.Properties using (toDigits-injective; showDigit-injective)
-open import Function using (_∘_; Injective)
+open import Function using (_∘_)
 import Data.List.Properties as Listₚ
 open import Data.Nat.Base using (ℕ)
 open import Data.Nat.Properties using (_≤?_)

From 228c20cebc734f152afea40f5408510a6a5c04f0 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 29 Jun 2023 09:47:06 +0100
Subject: [PATCH 35/80] simplified dependencies

---
 src/Data/Nat/Show/Properties.agda | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/Data/Nat/Show/Properties.agda b/src/Data/Nat/Show/Properties.agda
index fa120642cb..e397d9ea8c 100644
--- a/src/Data/Nat/Show/Properties.agda
+++ b/src/Data/Nat/Show/Properties.agda
@@ -6,15 +6,14 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Data.Digit using (showDigit; toDigits)
 open import Data.Digit.Properties using (toDigits-injective; showDigit-injective)
-open import Function using (_∘_)
 import Data.List.Properties as Listₚ
 open import Data.Nat.Base using (ℕ)
 open import Data.Nat.Properties using (_≤?_)
+open import Data.Nat.Show using (charsInBase)
+open import Function using (_∘_)
 open import Relation.Nullary.Decidable using (True)
 open import Relation.Binary.PropositionalEquality using (_≡_)
-open import Data.Nat.Show using (charsInBase)
 
 module Data.Nat.Show.Properties where
 

From 09a1e581e13ce775e1e98a024657f2bcccbc9a43 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 29 Jun 2023 09:49:19 +0100
Subject: [PATCH 36/80] irrelevant argument

---
 src/Data/Nat/Base.agda | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda
index 43faae290e..03c268fa3b 100644
--- a/src/Data/Nat/Base.agda
+++ b/src/Data/Nat/Base.agda
@@ -262,10 +262,7 @@ lessThanSuc : ∀ {n} → LessThan n (suc n)
 lessThanSuc {zero}  = _
 lessThanSuc {suc n} = lessThanSuc {n}
 
-lessThanSucSuc : ∀ {m n} → ⦃ LessThan m n ⦄ → LessThan (suc m) (suc n)
-{-
-lessThanSucSuc ⦃ lt ⦄ = lt
--}
+lessThanSucSuc : ∀ {m n} → .⦃ LessThan m n ⦄ → LessThan (suc m) (suc n)
 lessThanSucSuc {zero}  {suc _} = _
 lessThanSucSuc {suc m} {suc n} = lessThanSucSuc {m} {n}
 

From 38f823b0c595b35e9be25ab6befe7ca3ed5f44d3 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 29 Jun 2023 10:00:30 +0100
Subject: [PATCH 37/80] updated `CHANGELOG` and deprecations

---
 CHANGELOG.md                      | 10 +++++++---
 src/Data/Nat/Properties/Core.agda |  6 +++---
 2 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index ad04db38d1..6e863cf659 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1008,7 +1008,7 @@ Deprecated modules
 
 ### Deprecation of `Data.Nat.Properties.Core`
 
-* The module `Data.Nat.Properties.Core` has been deprecated, and its one entry moved to `Data.Nat.Properties`
+* The module `Data.Nat.Properties.Core` has been deprecated, and its one lemma moved to `Data.Nat.Base`, renamed as `s≤s⁻¹`
 
 Deprecated names
 ----------------
@@ -1234,6 +1234,8 @@ Deprecated names
 * In `Data.Nat.Properties`:
   ```
   suc[pred[n]]≡n  ↦  suc-pred
+  ≤-pred ↦ s≤s⁻¹
+  <-pred ↦ s<s⁻¹
   ≤-step          ↦  m≤n⇒m≤1+n
   ≤-stepsˡ        ↦  m≤n⇒m≤o+n
   ≤-stepsʳ        ↦  m≤n⇒m≤n+o
@@ -2159,9 +2161,11 @@ Other minor changes
   s<s⁻¹ : suc m < suc n → m < n
 
   LessThan : Rel ℕ 0ℓ
-  <ᵇ-lessThan   : .(T (m <ᵇ n)) → LessThan m n
+  instance lessThan : LessThan 0 (suc n)
+  lessThanSuc       : LessThan n (suc n)
+  lessThanSucSuc    : .⦃ LessThan m n ⦄ → LessThan (suc m) (suc n)
+
   <-lessThan    : .(m < n) → LessThan m n
-  <ᵇ-lessThan⁻¹ : .{{LessThan m n}} → T (m <ᵇ n)
   <-lessThan⁻¹  : .{{LessThan m n}} → m < n
 
   pattern <′-base          = ≤′-refl
diff --git a/src/Data/Nat/Properties/Core.agda b/src/Data/Nat/Properties/Core.agda
index 94031fdc37..66bfdaa32b 100644
--- a/src/Data/Nat/Properties/Core.agda
+++ b/src/Data/Nat/Properties/Core.agda
@@ -2,7 +2,7 @@
 -- The Agda standard library
 --
 -- This module is DEPRECATED. Please use
--- `Data.Nat.Properties` directly.
+-- `Data.Nat.Base directly.
 --
 ------------------------------------------------------------------------
 
@@ -12,7 +12,7 @@ module Data.Nat.Properties.Core where
 
 {-# WARNING_ON_IMPORT
 "Data.Nat.Properties.Core was deprecated in v2.0.
-Use Data.Nat.Properties instead."
+Use Data.Nat.Base instead."
 #-}
 
 open import Data.Nat.Base
@@ -22,4 +22,4 @@ open import Data.Nat.Base
 ------------------------------------------------------------------------
 
 ≤-pred : ∀ {m n} → suc m ≤ suc n → m ≤ n
-≤-pred (s≤s m≤n) = m≤n
+≤-pred = s≤s⁻¹

From 23cc8d6b413080193638dba46857ed8c46de13ea Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 29 Jun 2023 10:07:52 +0100
Subject: [PATCH 38/80] attempt at resolving merge conflicts

---
 src/Data/Fin/Base.agda       | 2 +-
 src/Data/Fin/Properties.agda | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda
index a453649c5f..64e623ef61 100644
--- a/src/Data/Fin/Base.agda
+++ b/src/Data/Fin/Base.agda
@@ -14,7 +14,7 @@ module Data.Fin.Base where
 open import Data.Bool.Base using (Bool; true; false; T; not)
 open import Data.Empty using (⊥-elim)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
-open import Data.Product as Product using (_×_; _,_; proj₁; proj₂)
+open import Data.Product.Base as Product using (_×_; _,_; proj₁; proj₂)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (id; _∘_; _on_; flip)
 open import Level using (0ℓ)
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 9c14dd4483..fb64235337 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -23,8 +23,8 @@ open import Data.Nat.Base as ℕ
 import Data.Nat.Properties as ℕₚ
 open import Data.Nat.Solver
 open import Data.Unit using (⊤; tt)
-open import Data.Product
-  using (Σ-syntax; ∃; ∃₂; ∄; _×_; _,_; map; proj₁; proj₂; uncurry; <_,_>)
+open import Data.Product as Prod
+  using (∃; ∃₂; _×_; _,_; map; proj₁; proj₂; uncurry; <_,_>)
 open import Data.Product.Properties using (,-injective)
 open import Data.Product.Algebra using (×-cong)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]; [_,_]′)
@@ -722,7 +722,7 @@ splitAt-≥ (suc m) (suc i) i≥m = cong (Sum.map suc id) (splitAt-≥ m i (ℕ.
 remQuot-combine : ∀ {n k} (i : Fin n) j → remQuot k (combine i j) ≡ (i , j)
 remQuot-combine {suc n} {k} zero    j rewrite splitAt-↑ˡ k j (n ℕ.* k) = refl
 remQuot-combine {suc n} {k} (suc i) j rewrite splitAt-↑ʳ k   (n ℕ.* k) (combine i j) =
-  cong (Data.Product.map₁ suc) (remQuot-combine i j)
+  cong (Prod.map₁ suc) (remQuot-combine i j)
 
 combine-remQuot : ∀ {n} k (i : Fin (n ℕ.* k)) → uncurry combine (remQuot {n} k i) ≡ i
 combine-remQuot {suc n} k i with splitAt k i in eq

From 27415e0bf7b595ac599cd77b8e1e90f644203949 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 6 Aug 2023 13:40:38 +0100
Subject: [PATCH 39/80] typo during merge conflict resolution

---
 src/Data/Vec/Relation/Unary/Linked/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Vec/Relation/Unary/Linked/Properties.agda b/src/Data/Vec/Relation/Unary/Linked/Properties.agda
index c75864e89a..69024b1b51 100644
--- a/src/Data/Vec/Relation/Unary/Linked/Properties.agda
+++ b/src/Data/Vec/Relation/Unary/Linked/Properties.agda
@@ -16,7 +16,7 @@ open import Data.Vec.Relation.Unary.Linked as Linked
 open import Data.Fin.Base using (zero; suc; _<_)
 open import Data.Nat.Base using (ℕ; zero; suc; s<s⁻¹)
 open import Level using (Level)
-pen import Function.Base using (_on_)
+open import Function.Base using (_on_)
 open import Relation.Binary using (Rel; Transitive)
 open import Relation.Unary using (Pred; Decidable)
 

From d0421e88d7fc62a63e7431ba4865247aaf045ec4 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 6 Aug 2023 13:47:57 +0100
Subject: [PATCH 40/80] more errors introduced during merge conflict resolution

---
 src/Data/Nat/Properties.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 5cb40c89bc..1f6d39c7f2 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -35,7 +35,7 @@ open import Relation.Binary.Consequences using (flip-Connex)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary hiding (Irrelevant)
 open import Relation.Nullary.Decidable using (True; via-injection; map′)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Reflects using (fromEquivalence)
 
 open import Algebra.Definitions {A = ℕ} _≡_
@@ -2170,7 +2170,7 @@ module _ {p} {P : Pred ℕ p} (P? : U.Decidable P) where
   ... | _      | yes (n , n<v , Pn) = yes (n , m≤n⇒m≤1+n n<v , Pn)
   ... | no ¬Pv | no ¬Pn<v           = no ¬Pn<1+v
     where
-    ¬Pn<1+v : (∃ λ n → n < suc v × P n) → ⊥
+    ¬Pn<1+v : ¬ (∃ λ n → n < suc v × P n)
     ¬Pn<1+v (n , s≤s n≤v , Pn) with n ≟ v
     ... | yes refl = ¬Pv Pn
     ... | no  n≢v  = ¬Pn<v (n , ≤∧≢⇒< n≤v n≢v , Pn)

From 2f260c91857a39ef9f2ebab1371ca1441435f637 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 6 Aug 2023 13:58:30 +0100
Subject: [PATCH 41/80] another error introduced during merge conflict
 resolution

---
 src/Data/Nat/Show/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Nat/Show/Properties.agda b/src/Data/Nat/Show/Properties.agda
index cc30c6aaec..13dd34ace2 100644
--- a/src/Data/Nat/Show/Properties.agda
+++ b/src/Data/Nat/Show/Properties.agda
@@ -13,7 +13,7 @@ open import Data.Nat.Properties using (_≤?_)
 open import Data.Nat.Show using (charsInBase)
 open import Function.Base using (_∘_)
 open import Relation.Nullary.Decidable using (True)
-pen import Relation.Binary.PropositionalEquality.Core using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
 module Data.Nat.Show.Properties where
 

From aedd6d4258045a2ae8b92248aae7472e5f33c3c0 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 11 Aug 2023 10:20:38 +0100
Subject: [PATCH 42/80] lightened imports ahead of merge conflict resolution

---
 src/Data/Vec/Relation/Unary/Linked/Properties.agda | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Data/Vec/Relation/Unary/Linked/Properties.agda b/src/Data/Vec/Relation/Unary/Linked/Properties.agda
index 69024b1b51..8ff5a4d2e3 100644
--- a/src/Data/Vec/Relation/Unary/Linked/Properties.agda
+++ b/src/Data/Vec/Relation/Unary/Linked/Properties.agda
@@ -17,7 +17,8 @@ open import Data.Fin.Base using (zero; suc; _<_)
 open import Data.Nat.Base using (ℕ; zero; suc; s<s⁻¹)
 open import Level using (Level)
 open import Function.Base using (_on_)
-open import Relation.Binary using (Rel; Transitive)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Definitions using (Transitive)
 open import Relation.Unary using (Pred; Decidable)
 
 private

From 988ae2197fa494d40e5369d30114a93d7c73f33d Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 16 Aug 2023 09:56:24 +0100
Subject: [PATCH 43/80] =?UTF-8?q?made=20som=20e=20proofs=20lazier=20in=20t?=
 =?UTF-8?q?heir=20`=5F=E2=89=A4=5F`=20arguments?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Data/Vec/Properties.agda | 19 ++++++++++---------
 1 file changed, 10 insertions(+), 9 deletions(-)

diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 49924a7b31..df6799c212 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -215,12 +215,13 @@ lookup⇒[]= (suc i) (_ ∷ xs) p    = there (lookup⇒[]= i xs p)
 
 lookup-inject≤-take : ∀ m (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m + n)) →
                       lookup xs (Fin.inject≤ i m≤m+n) ≡ lookup (take m xs) i
-lookup-inject≤-take (suc m) m≤m+n zero (x ∷ xs)
+lookup-inject≤-take (suc m) _ zero (x ∷ xs)
   rewrite unfold-take m x xs = refl
-lookup-inject≤-take (suc (suc m)) (s≤s m≤m+n) (suc zero) (x ∷ y ∷ xs)
-  rewrite unfold-take (suc m) x (y ∷ xs) | unfold-take m y xs = refl
-lookup-inject≤-take (suc (suc m)) (s≤s (s≤s m≤m+n)) (suc (suc i)) (x ∷ y ∷ xs)
-  rewrite unfold-take (suc m) x (y ∷ xs) | unfold-take m y xs = lookup-inject≤-take m m≤m+n i xs
+lookup-inject≤-take (suc (suc m)) m≤m+n (suc i) (x ∷ y ∷ xs)
+  rewrite unfold-take (suc m) x (y ∷ xs) | unfold-take m y xs
+  with i
+... | zero = refl
+... | suc j = lookup-inject≤-take m (s≤s⁻¹ (s≤s⁻¹ m≤m+n)) j xs
 
 ------------------------------------------------------------------------
 -- updateAt (_[_]%=_)
@@ -480,14 +481,14 @@ map-⊛ f g (x ∷ xs) = cong (f x (g x) ∷_) (map-⊛ f g xs)
 lookup-++-< : ∀ (xs : Vec A m) (ys : Vec A n) →
               ∀ i (i<m : toℕ i < m) →
               lookup (xs ++ ys) i  ≡ lookup xs (Fin.fromℕ< i<m)
-lookup-++-< (x ∷ xs) ys zero    z<s       = refl
-lookup-++-< (x ∷ xs) ys (suc i) (s<s i<m) = lookup-++-< xs ys i i<m
+lookup-++-< (x ∷ xs) ys zero    _     = refl
+lookup-++-< (x ∷ xs) ys (suc i) si<sm = lookup-++-< xs ys i (s<s⁻¹ si<sm)
 
 lookup-++-≥ : ∀ (xs : Vec A m) (ys : Vec A n) →
               ∀ i (i≥m : toℕ i ≥ m) →
               lookup (xs ++ ys) i ≡ lookup ys (Fin.reduce≥ i i≥m)
-lookup-++-≥ []       ys i       i≥m       = refl
-lookup-++-≥ (x ∷ xs) ys (suc i) (s≤s i≥m) = lookup-++-≥ xs ys i i≥m
+lookup-++-≥ []       ys i       _     = refl
+lookup-++-≥ (x ∷ xs) ys (suc i) si≥sm = lookup-++-≥ xs ys i (s≤s⁻¹ si≥sm)
 
 lookup-++ˡ : ∀ (xs : Vec A m) (ys : Vec A n) i →
              lookup (xs ++ ys) (i ↑ˡ n) ≡ lookup xs i

From e8822d4e8a263fa8cde4f357826cdc4cfd021a58 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 29 Sep 2023 08:14:40 +0100
Subject: [PATCH 44/80] simplfied `import`s

---
 src/Data/Fin/Base.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda
index 82e9109dc8..8a824e60dd 100644
--- a/src/Data/Fin/Base.agda
+++ b/src/Data/Fin/Base.agda
@@ -12,7 +12,6 @@
 module Data.Fin.Base where
 
 open import Data.Bool.Base using (Bool; true; false; T; not)
-open import Data.Empty using (⊥-elim)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc; z≤n; s≤s; z<s; s<s; _^_)
 open import Data.Product.Base as Product using (_×_; _,_; proj₁; proj₂)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
@@ -21,6 +20,7 @@ open import Level using (0ℓ)
 open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong)
 open import Relation.Binary.Indexed.Heterogeneous.Core using (IRel)
+open import Relation.Nullary.Negation.Core using (contradiction)
 
 private
   variable

From bf2b3bb493967a7d77ad877afbc5596afe1b03d5 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 29 Sep 2023 08:17:20 +0100
Subject: [PATCH 45/80] knock-on consequence of merge conflict resolution

---
 src/Data/Nat/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 8cb115856c..cb175d9cf2 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -116,7 +116,7 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n))
 -- Properties of LessThan
 ------------------------------------------------------------------------
 
-lessThan? : B.Decidable LessThan
+lessThan? : Decidable LessThan
 lessThan? m       zero    = no λ()
 lessThan? zero    (suc n) = yes _
 lessThan? (suc m) (suc n) = lessThan? m n

From 7a6ad62c969b45b544d7c4187a519ace282c1740 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 29 Sep 2023 08:22:44 +0100
Subject: [PATCH 46/80] simplified irrelevance proof

---
 src/Data/Fin/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 1c75f12056..5e8656f9e1 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -650,7 +650,7 @@ inject≤-injective {n = suc _} p q (suc i) (suc j) eq =
 
 inject≤-irrelevant : ∀ (m≤n m≤n′ : m ℕ.≤ n) i →
                     inject≤ i m≤n ≡ inject≤ i m≤n′
-inject≤-irrelevant m≤n m≤n′ i =  cong (inject≤ i) (ℕₚ.≤-irrelevant m≤n m≤n′)
+inject≤-irrelevant m≤n m≤n′ i = refl
 
 ------------------------------------------------------------------------
 -- pred

From afca20f76f24f10aa9ed848fb1e557a6f886eb4f Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 29 Sep 2023 08:26:15 +0100
Subject: [PATCH 47/80] simplified irrelevance proof

---
 src/Data/Vec/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 45d30e9256..45ff2a296d 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -1306,7 +1306,7 @@ lookup-inject≤-take m m≤m+n i xs = sym (begin
   lookup (take m xs) i
     ≡⟨ lookup-take-inject≤ xs i ⟩
   lookup xs (Fin.inject≤ i _)
-    ≡⟨ cong ((lookup xs) ∘ (Fin.inject≤ i)) (≤-irrelevant _ _) ⟩
+    ≡⟨⟩
   lookup xs (Fin.inject≤ i m≤m+n)
     ∎) where open ≡-Reasoning
 {-# WARNING_ON_USAGE lookup-inject≤-take

From 34155ca252f88d446fb0b65f8ff54c32bf7fbe81 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 29 Sep 2023 08:28:50 +0100
Subject: [PATCH 48/80] typo

---
 src/Data/Vec/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 45ff2a296d..72276908ee 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -1293,7 +1293,7 @@ Please use take-map instead."
 drop-distr-zipWith = drop-zipWith
 {-# WARNING_ON_USAGE drop-distr-zipWith
 "Warning: drop-distr-zipWith was deprecated in v2.0.
-Please use tdrop-zipWith instead."
+Please use drop-zipWith instead."
 #-}
 drop-distr-map = drop-map
 {-# WARNING_ON_USAGE drop-distr-map

From 5e8a4a62b64a3f10154a6514c08cef087749a663 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 29 Sep 2023 08:33:20 +0100
Subject: [PATCH 49/80] simplified injectivity proof

---
 src/Data/Fin/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 5e8656f9e1..faedccb0e6 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -642,7 +642,7 @@ inject≤-trans : ∀ (i : Fin m) (m≤n : m ℕ.≤ n) (n≤o : n ℕ.≤ o) 
                 inject≤ (inject≤ i m≤n) n≤o ≡ inject≤ i (ℕₚ.≤-trans m≤n n≤o)
 inject≤-trans i m≤n n≤o = inject≤-idempotent i m≤n n≤o _
 
-inject≤-injective : ∀ (m≤n m≤n′ : m ℕ.≤ n) i j →
+inject≤-injective : ∀ .(m≤n m≤n′ : m ℕ.≤ n) i j →
                     inject≤ i m≤n ≡ inject≤ j m≤n′ → i ≡ j
 inject≤-injective {n = suc _} p q zero    zero    eq = refl
 inject≤-injective {n = suc _} p q (suc i) (suc j) eq =

From 2d102b14a31625d5681b98e3eb08b9fb8f5bd5c4 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 29 Sep 2023 08:40:06 +0100
Subject: [PATCH 50/80] knock-on changes; further simplified `import`s

---
 src/Data/Digit/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Digit/Properties.agda b/src/Data/Digit/Properties.agda
index 113bdde6ca..fb52d2af72 100644
--- a/src/Data/Digit/Properties.agda
+++ b/src/Data/Digit/Properties.agda
@@ -15,7 +15,7 @@ open import Data.Product.Base using (_,_; proj₁)
 open import Data.Vec.Relation.Unary.Unique.Propositional using (Unique)
 import Data.Vec.Relation.Unary.Unique.Propositional.Properties as Uniqueₚ
 open import Data.Vec.Relation.Unary.AllPairs using (allPairs?)
-open import Relation.Nullary.Decidable using (True; from-yes; ¬?)
+open import Relation.Nullary.Decidable.Core using (True; from-yes; ¬?)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 open import Function.Base using (_∘_)
 

From 57c80e2010f2516fded56ab48b5315703cba766d Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 29 Sep 2023 08:52:34 +0100
Subject: [PATCH 51/80] knock-on changes; further simplified `import`s

---
 src/Data/Fin/Properties.agda | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index faedccb0e6..25e411f298 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -43,10 +43,10 @@ open import Relation.Binary.Structures
   using (IsDecEquivalence; IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder)
 open import Relation.Binary.PropositionalEquality as P
   using (_≡_; _≢_; refl; sym; trans; cong; cong₂; subst; _≗_; module ≡-Reasoning)
-open import Relation.Nullary
-  using (Reflects; ofʸ; ofⁿ; Dec; _because_; does; proof; yes; no; ¬_; _×-dec_; _⊎-dec_; contradiction)
-open import Relation.Nullary.Reflects
-open import Relation.Nullary.Decidable as Dec using (map′)
+open import Relation.Nullary.Decidable as Dec
+  using (Dec; _because_; yes; no; _×-dec_; _⊎-dec_; map′)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
+open import Relation.Nullary.Reflects using (Reflects; invert)
 open import Relation.Unary as U
   using (U; Pred; Decidable; _⊆_; Satisfiable; Universal)
 open import Relation.Unary.Properties using (U?)
@@ -1065,8 +1065,8 @@ private
   -- The boolean component of the result is exactly the
   -- obvious fold of boolean tests (`foldr _∧_ true`).
   note : ∀ {p} {P : Pred (Fin 3) p} (P? : Decidable P) →
-         ∃ λ z → does (all? P?) ≡ z
-  note P? = does (P? 0F) ∧ does (P? 1F) ∧ does (P? 2F) ∧ true
+         ∃ λ z → Dec.does (all? P?) ≡ z
+  note P? = Dec.does (P? 0F) ∧ Dec.does (P? 1F) ∧ Dec.does (P? 2F) ∧ true
           , refl
 
 -- If a decidable predicate P over a finite set is sometimes false,

From 754eefd64d535f6b4a65684ce0dc67d957498188 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 29 Sep 2023 09:00:11 +0100
Subject: [PATCH 52/80] knock-on changes; further simplified `import`s

---
 src/Data/Fin/Base.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda
index 8a824e60dd..de1998b5e7 100644
--- a/src/Data/Fin/Base.agda
+++ b/src/Data/Fin/Base.agda
@@ -11,8 +11,8 @@
 
 module Data.Fin.Base where
 
-open import Data.Bool.Base using (Bool; true; false; T; not)
-open import Data.Nat.Base as ℕ using (ℕ; zero; suc; z≤n; s≤s; z<s; s<s; _^_)
+open import Data.Bool.Base using (Bool; T)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
 open import Data.Product.Base as Product using (_×_; _,_; proj₁; proj₂)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (id; _∘_; _on_; flip)

From 27712f8d913753dcad0e12292ef73dab2b5a62a5 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 29 Sep 2023 09:02:48 +0100
Subject: [PATCH 53/80] knock-on changes; further simplified `import`s

---
 src/Data/Vec/Base.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda
index 507ac05463..0ef297392d 100644
--- a/src/Data/Vec/Base.agda
+++ b/src/Data/Vec/Base.agda
@@ -8,7 +8,7 @@
 
 module Data.Vec.Base where
 
-open import Data.Bool.Base using (Bool; true; false; if_then_else_)
+open import Data.Bool.Base using (Bool; if_then_else_)
 open import Data.Nat.Base
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.List.Base as List using (List)

From 3f6fb748112f10905234089e7e3c84f3cdb21492 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 29 Sep 2023 09:10:09 +0100
Subject: [PATCH 54/80] knock-on changes; further simplified `import`s

---
 src/Data/Vec/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 72276908ee..6e4f18f03e 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -29,7 +29,7 @@ open import Relation.Binary.Definitions using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality
   using (_≡_; _≢_; _≗_; refl; sym; trans; cong; cong₂; subst; module ≡-Reasoning)
 open import Relation.Unary using (Pred; Decidable)
-open import Relation.Nullary.Decidable.Core using (Dec; does; yes; no; _×-dec_; map′)
+open import Relation.Nullary.Decidable.Core using (Dec; does; yes; _×-dec_; map′)
 open import Relation.Nullary.Negation.Core using (contradiction)
 
 open ≡-Reasoning

From ee823acc8f610a34e2c770210d40587dd7703b5b Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 29 Sep 2023 09:37:45 +0100
Subject: [PATCH 55/80] simplified proof(s)

---
 src/Data/Nat/Properties.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index cb175d9cf2..eb811af952 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -721,8 +721,8 @@ m<n+m : ∀ m {n} → n > 0 → m < n + m
 m<n+m m {n} n>0 rewrite +-comm n m = m<m+n m n>0
 
 m+n≮n : ∀ m n → m + n ≮ n
-m+n≮n zero    n                   = n≮n n
-m+n≮n (suc m) (suc n) (s<s m+n<n) = m+n≮n m (suc n) (m<n⇒m<1+n m+n<n)
+m+n≮n zero    n                = n≮n n
+m+n≮n (suc m) n@(suc _) sm+n<n = m+n≮n m n (m<n⇒m<1+n (s<s⁻¹ sm+n<n))
 
 m+n≮m : ∀ m n → m + n ≮ m
 m+n≮m m n = subst (_≮ m) (+-comm n m) (m+n≮n n m)

From 1c82b4551adb7709e13be6624610ad4bc4993b8d Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 29 Sep 2023 12:17:08 +0100
Subject: [PATCH 56/80] removed `LessThan` from `Nat.Base`

---
 CHANGELOG.md           | 40 ++++++++++++++++------------------------
 src/Data/Nat/Base.agda | 39 +--------------------------------------
 2 files changed, 17 insertions(+), 62 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index cb55dc1853..314d8450d5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -280,7 +280,7 @@ Non-backwards compatible changes
   Data.Sum.Function.Setoid
   Data.Sum.Function.Propositional
   ```
-  
+
 * Additionally the following proofs now use the new definitions instead of the old ones:
   * `Algebra.Lattice.Properties.BooleanAlgebra`
   * `Algebra.Properties.CommutativeMonoid.Sum`
@@ -360,8 +360,8 @@ Non-backwards compatible changes
 * The module `Function.Definitions` no longer has two equalities as module arguments, as
   they did not interact as intended with the re-exports from `Function.Definitions.(Core1/Core2)`.
   The latter have been removed and their definitions folded into `Function.Definitions`.
-  
-* In `Function.Definitions` the types of `Surjective`, `Injective` and `Surjective` 
+
+* In `Function.Definitions` the types of `Surjective`, `Injective` and `Surjective`
   have been changed from:
   ```
   Surjective f = ∀ y → ∃ λ x → f x ≈₂ y
@@ -376,16 +376,16 @@ Non-backwards compatible changes
   ```
   This is for several reasons: i) the new definitions compose much more easily, ii) Agda
   can better infer the equalities used.
-  
+
   To ease backwards compatibility:
-   - the old definitions have been moved to the new names  `StrictlySurjective`, 
-	 `StrictlyInverseˡ` and `StrictlyInverseʳ`. 
-   - The records in  `Function.Structures` and `Function.Bundles` export proofs 
-	 of these under the names `strictlySurjective`, `strictlyInverseˡ` and 
-	 `strictlyInverseʳ`,
+   - the old definitions have been moved to the new names  `StrictlySurjective`,
+         `StrictlyInverseˡ` and `StrictlyInverseʳ`.
+   - The records in  `Function.Structures` and `Function.Bundles` export proofs
+         of these under the names `strictlySurjective`, `strictlyInverseˡ` and
+         `strictlyInverseʳ`,
    - Conversion functions have been added in both directions to
-	 `Function.Consequences(.Propositional)`. 
-  
+         `Function.Consequences(.Propositional)`.
+
 #### Proofs of non-zeroness/positivity/negativity as instance arguments
 
 * Many numeric operations in the library require their arguments to be non-zero,
@@ -772,14 +772,14 @@ Non-backwards compatible changes
 ### Changes to triple reasoning interface
 
 * The module `Relation.Binary.Reasoning.Base.Triple` now takes an extra proof that the strict
-  relation is irreflexive. 
-  
+  relation is irreflexive.
+
 * This allows the following new proof combinator:
   ```agda
   begin-contradiction : (r : x IsRelatedTo x) → {s : True (IsStrict? r)} → A
   ```
   that takes a proof that a value is strictly less than itself and then applies the principle of explosion.
-  
+
 * Specialised versions of this combinator are available in the following derived modules:
   ```
   Data.Nat.Properties
@@ -1465,7 +1465,7 @@ Deprecated names
   take-distr-map     ↦  take-map
   drop-distr-zipWith ↦  drop-zipWith
   drop-distr-map     ↦  drop-map
-  
+
   updateAt-id-relative      ↦  updateAt-id-local
   updateAt-compose-relative ↦  updateAt-∘-local
   updateAt-compose          ↦  updateAt-∘
@@ -2349,7 +2349,7 @@ Additions to existing modules
 
   length-isMagmaHomomorphism  : (A : Set a) → IsMagmaHomomorphism (++-rawMagma A) +-rawMagma length
   length-isMonoidHomomorphism : (A : Set a) → IsMonoidHomomorphism (++-[]-rawMonoid A) +-0-rawMonoid length
-  
+
   take-map : take n (map f xs) ≡ map f (take n xs)
   drop-map : drop n (map f xs) ≡ map f (drop n xs)
   head-map : head (map f xs) ≡ Maybe.map f (head xs)
@@ -2377,14 +2377,6 @@ Additions to existing modules
   s≤s⁻¹ : suc m ≤ suc n → m ≤ n
   s<s⁻¹ : suc m < suc n → m < n
 
-  LessThan : Rel ℕ 0ℓ
-  instance lessThan : LessThan 0 (suc n)
-  lessThanSuc       : LessThan n (suc n)
-  lessThanSucSuc    : .⦃ LessThan m n ⦄ → LessThan (suc m) (suc n)
-
-  <-lessThan    : .(m < n) → LessThan m n
-  <-lessThan⁻¹  : .{{LessThan m n}} → m < n
-
   pattern <′-base          = ≤′-refl
   pattern <′-step {n} m<′n = ≤′-step {n} m<′n
 
diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda
index 6163d4d2ad..01abccb8e1 100644
--- a/src/Data/Nat/Base.agda
+++ b/src/Data/Nat/Base.agda
@@ -245,44 +245,7 @@ suc n ! = suc n * n !
 -- Alternative definitions of _≤_/_<_
 
 ------------------------------------------------------------------------
--- Another useful (proof-irrelevant) definition of _<_
-
-LessThan : Rel ℕ 0ℓ
-LessThan m n = T (m <ᵇ n)
-
--- instance
-
-instance
-  lessThan : ∀ {n} → LessThan 0 (suc n)
-  lessThan = _
-
--- Constructors
-
-lessThanSuc : ∀ {n} → LessThan n (suc n)
-lessThanSuc {zero}  = _
-lessThanSuc {suc n} = lessThanSuc {n}
-
-lessThanSucSuc : ∀ {m n} → .⦃ LessThan m n ⦄ → LessThan (suc m) (suc n)
-lessThanSucSuc {zero}  {suc _} = _
-lessThanSucSuc {suc m} {suc n} = lessThanSucSuc {m} {n}
-
-<-lessThan : ∀ {m n} → .(m<n : m < n) → LessThan m n
-<-lessThan {zero}  {suc n}       = _
-<-lessThan {suc m} {suc n} (m<n) = <-lessThan {m} {n} (s<s⁻¹ m<n)
-
-<″-lessThan : ∀ {m n} → LessThan m (suc m + n)
-<″-lessThan {zero}    = _
-<″-lessThan {suc m} = <″-lessThan {m}
-
--- Destructors
-
-<-lessThan⁻¹ : ∀ m {n} → .⦃ LessThan m n ⦄ → m < n
-<-lessThan⁻¹ zero    {suc n} = z<s
-<-lessThan⁻¹ (suc m) {suc n} = s<s (<-lessThan⁻¹ m)
-
-
-------------------------------------------------------------------------
--- Another alternative definition of _≤_
+-- An alternative definition of _≤_
 
 -- The following definition of _≤_ is more suitable for well-founded
 -- induction (see Data.Nat.Induction)

From 697cbc0134b1594738af744be600c943691016bf Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 29 Sep 2023 12:20:46 +0100
Subject: [PATCH 57/80] removed `LessThan` from `Nat.Properties`

---
 src/Data/Nat/Properties.agda | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index eb811af952..8977a716ab 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -112,15 +112,6 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n))
 1+n≢n : ∀ {n} → suc n ≢ n
 1+n≢n {suc n} = 1+n≢n ∘ suc-injective
 
-------------------------------------------------------------------------
--- Properties of LessThan
-------------------------------------------------------------------------
-
-lessThan? : Decidable LessThan
-lessThan? m       zero    = no λ()
-lessThan? zero    (suc n) = yes _
-lessThan? (suc m) (suc n) = lessThan? m n
-
 ------------------------------------------------------------------------
 -- Properties of _<ᵇ_
 ------------------------------------------------------------------------

From 4ef993894910bb26d883f3c1ab72da82b76243d4 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 29 Sep 2023 12:30:33 +0100
Subject: [PATCH 58/80] removed `LessThan` from `Fin.Base`

---
 src/Data/Fin/Base.agda | 15 ++-------------
 1 file changed, 2 insertions(+), 13 deletions(-)

diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda
index de1998b5e7..ffe55a89b4 100644
--- a/src/Data/Fin/Base.agda
+++ b/src/Data/Fin/Base.agda
@@ -65,22 +65,11 @@ fromℕ : (n : ℕ) → Fin (suc n)
 fromℕ zero    = zero
 fromℕ (suc n) = suc (fromℕ n)
 
--- fromℕLessThan m ⦃_⦄ = "m".
-
-fromℕLessThan : ∀ m {n} → .⦃ ℕ.LessThan m n ⦄ → Fin n
-fromℕLessThan zero    {suc _} = zero
-fromℕLessThan (suc m) {suc _} = suc (fromℕLessThan m)
-
--- fromℕ<′ m ⦃_⦄ = "m".
-
-fromℕ<′ : ∀ m {n} → .⦃ m ℕ.< n ⦄ → Fin n
-fromℕ<′ m {n} ⦃ m<n ⦄ = fromℕLessThan m {n}
-  where instance _ = ℕ.<-lessThan m<n
-
 -- fromℕ< {m} _ = "m".
 
 fromℕ< : ∀ {m n} → .(m ℕ.< n) → Fin n
-fromℕ< {m} m<n = fromℕ<′ m ⦃ m<n ⦄
+fromℕ< {zero}  {n = suc _} _   = zero
+fromℕ< {suc m} {n = suc _} m<n = suc (fromℕ< (ℕ.s<s⁻¹ m<n))
 
 -- fromℕ<″ m _ = "m".
 

From 808d89bcdc06abf3775d28958e2f943b56f1e3d9 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 29 Sep 2023 13:11:24 +0100
Subject: [PATCH 59/80] removed `LessThan` from `Fin.Properties`

---
 src/Data/Fin/Properties.agda | 163 ++++++++---------------------------
 1 file changed, 34 insertions(+), 129 deletions(-)

diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 25e411f298..d38c53fc99 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -162,12 +162,9 @@ toℕ-↑ʳ (suc n) i = cong suc (toℕ-↑ʳ n i)
 -- toℕ and the ordering relations
 ------------------------------------------------------------------------
 
-toℕ-LessThan : (i : Fin n) → ℕ.LessThan (toℕ i) n
-toℕ-LessThan zero    = _
-toℕ-LessThan (suc i) = toℕ-LessThan i
-
-toℕ<n : (i : Fin n) → toℕ i ℕ.< n
-toℕ<n {n = suc _} i = ℕ.<-lessThan⁻¹ (toℕ i) ⦃ toℕ-LessThan i ⦄
+toℕ<n : ∀ (i : Fin n) → toℕ i ℕ.< n
+toℕ<n {n = suc _} zero    = z<s
+toℕ<n {n = suc _} (suc i) = s<s (toℕ<n i)
 
 toℕ≤pred[n] : ∀ (i : Fin n) → toℕ i ℕ.≤ ℕ.pred n
 toℕ≤pred[n] zero                 = z≤n
@@ -175,10 +172,7 @@ toℕ≤pred[n] (suc {n = suc n} i)  = s≤s (toℕ≤pred[n] i)
 
 toℕ≤n : ∀ (i : Fin n) → toℕ i ℕ.≤ n
 toℕ≤n {suc n} i = ℕₚ.m≤n⇒m≤1+n (toℕ≤pred[n] i)
-{-
-toℕ<n : ∀ (i : Fin n) → toℕ i ℕ.< n
-toℕ<n {suc n} i = s<s (toℕ≤pred[n] i)
--}
+
 -- A simpler implementation of toℕ≤pred[n],
 -- however, with a different reduction behavior.
 -- If no one needs the reduction behavior of toℕ≤pred[n],
@@ -213,134 +207,51 @@ fromℕ-toℕ (suc i) = cong suc (fromℕ-toℕ i)
 ≤fromℕ : ∀ (i : Fin (suc n)) → i ≤ fromℕ n
 ≤fromℕ {n = n} i rewrite toℕ-fromℕ n = ℕ.s≤s⁻¹ (toℕ<n i)
 
-------------------------------------------------------------------------
--- fromℕLessThan
-------------------------------------------------------------------------
-
-fromℕLessThan-toℕ : ∀ (i : Fin n) → let instance _ = toℕ-LessThan i in
-                    fromℕLessThan (toℕ i) ≡ i
-fromℕLessThan-toℕ zero    = refl
-fromℕLessThan-toℕ (suc i) = cong suc (fromℕLessThan-toℕ i)
-
-toℕ-fromℕLessThan : ∀ m {n} .⦃ _ : ℕ.LessThan m n ⦄ → toℕ (fromℕLessThan m {n}) ≡ m
-toℕ-fromℕLessThan zero    {suc _} = refl
-toℕ-fromℕLessThan (suc m) {suc _} = cong suc (toℕ-fromℕLessThan m)
-
-fromℕLessThan-cong : ∀ {m n o} ⦃ m<o : _ ⦄ ⦃ n<o : _ ⦄ → m ≡ n →
-                     fromℕLessThan m {o} ⦃ m<o ⦄ ≡ fromℕLessThan n {o} ⦃ n<o ⦄
-fromℕLessThan-cong {zero}  {zero}          r = refl
-fromℕLessThan-cong {suc m} {suc n} {suc _} r
-  = cong suc (fromℕLessThan-cong {m} {n} (ℕₚ.suc-injective r))
-
-fromℕLessThan-injective : ∀ {m n o} ⦃ m<o : _ ⦄ ⦃ n<o : _ ⦄ →
-                          fromℕLessThan m {o} ⦃ m<o ⦄ ≡ fromℕLessThan n {o} ⦃ n<o ⦄ →
-                          m ≡ n
-fromℕLessThan-injective {zero}  {zero}          r = refl
-fromℕLessThan-injective {zero}  {suc n} {suc _} () -- unexpectedly necessary?
-fromℕLessThan-injective {suc m} {suc n} {suc _} r
-  = cong suc (fromℕLessThan-injective {m} {n} (suc-injective r))
-
--- fromℕ is a special case of fromℕLessThan.
-fromℕ-LessThan-def : ∀ n → let instance _ = ℕ.lessThanSuc {n} in
-                     fromℕ n ≡ fromℕLessThan n
-fromℕ-LessThan-def zero    = refl
-fromℕ-LessThan-def (suc n) = cong suc (fromℕ-LessThan-def n)
-
-------------------------------------------------------------------------
--- fromℕ<′
-------------------------------------------------------------------------
-
-fromℕ<′≡fromℕLessThan : ∀ {m n} → .⦃ m<n : m ℕ.< n ⦄ →
-                        let instance _ = ℕ.<-lessThan m<n in
-                        fromℕ<′ m ≡ fromℕLessThan m
-fromℕ<′≡fromℕLessThan = refl
-
-fromℕ<′-toℕ : (i : Fin n) → let instance _ = toℕ<n i in fromℕ<′ (toℕ i) ≡ i
-fromℕ<′-toℕ i = fromℕLessThan-toℕ i
-
-toℕ-fromℕ<′ : ∀ m {n} .⦃ m<n : m ℕ.< n ⦄ → toℕ (fromℕ<′ m ⦃ m<n ⦄) ≡ m
-toℕ-fromℕ<′ m {n} ⦃ m<n ⦄ = toℕ-fromℕLessThan m {n} ⦃ ℕ.<-lessThan m<n ⦄
-
-fromℕ<′-cong : ∀ {m n o} .⦃ m<o : m ℕ.< o ⦄ .⦃ n<o : n ℕ.< o ⦄ →
-               m ≡ n → fromℕ<′ m ≡ fromℕ<′ n
-fromℕ<′-cong ⦃ m<o ⦄ ⦃ n<o ⦄ r = fromℕLessThan-cong r
-  where
-    instance _ = ℕ.<-lessThan m<o
-    instance _ = ℕ.<-lessThan n<o
-
-fromℕ<′-injective : ∀ {m n o} ⦃ m<o : m ℕ.< o ⦄ ⦃ n<o : n ℕ.< o ⦄ →
-                    fromℕ<′ m {o} ⦃ m<o ⦄ ≡ fromℕ<′ n {o} ⦃ n<o ⦄ →
-                    m ≡ n
-fromℕ<′-injective ⦃ m<o ⦄ ⦃ n<o ⦄ r = fromℕLessThan-injective r
-  where
-    instance _ = ℕ.<-lessThan m<o
-    instance _ = ℕ.<-lessThan n<o
-
 ------------------------------------------------------------------------
 -- fromℕ<
 ------------------------------------------------------------------------
 
-fromℕ<≡fromℕLessThan : .⦃ m<n : m ℕ.< n ⦄ →
-                       let instance _ = ℕ.<-lessThan m<n in
-                       fromℕ< m<n ≡ fromℕLessThan m
-fromℕ<≡fromℕLessThan = fromℕ<′≡fromℕLessThan
+fromℕ<-toℕ : ∀ (i : Fin n) .(i<n : toℕ i ℕ.< n) → fromℕ< i<n ≡ i
+fromℕ<-toℕ zero    _   = refl
+fromℕ<-toℕ (suc i) i<n = cong suc (fromℕ<-toℕ i (ℕ.s<s⁻¹ i<n))
 
-fromℕ<-toℕ : (i : Fin n) .(i<n : toℕ i ℕ.< n) → fromℕ< i<n ≡ i
-fromℕ<-toℕ i i<n = begin
-  fromℕ< i<n
-    ≡⟨ fromℕ<≡fromℕLessThan ⦃ i<n ⦄ ⟩
-  fromℕLessThan (toℕ i)
-    ≡⟨ fromℕLessThan-toℕ i ⟩
-  i ∎ where open ≡-Reasoning ; instance _ = toℕ-LessThan i
+toℕ-fromℕ< : ∀ .(m<n : m ℕ.< n) → toℕ (fromℕ< m<n) ≡ m
+toℕ-fromℕ< {m = zero}  {n = suc _} _   = refl
+toℕ-fromℕ< {m = suc m} {n = suc _} m<n = cong suc (toℕ-fromℕ< (ℕ.s<s⁻¹ m<n))
 
-toℕ-fromℕ< : .(m<n : m ℕ.< n) → toℕ (fromℕ< m<n) ≡ m
-toℕ-fromℕ< {m = m} m<n = begin
-  toℕ (fromℕ< m<n)
-    ≡⟨ cong toℕ (fromℕ<≡fromℕLessThan ⦃ m<n ⦄) ⟩
-  toℕ (fromℕLessThan m)
-    ≡⟨ toℕ-fromℕLessThan m ⟩
-  m ∎ where open ≡-Reasoning; instance _ = ℕ.<-lessThan m<n
+-- fromℕ is a special case of fromℕ<.
+fromℕ-def : ∀ n → fromℕ n ≡ fromℕ< ℕₚ.≤-refl
+fromℕ-def zero    = refl
+fromℕ-def (suc n) = cong suc (fromℕ-def n)
 
 fromℕ<-cong : ∀ m n {o} → m ≡ n → .(m<o : m ℕ.< o) .(n<o : n ℕ.< o) →
               fromℕ< m<o ≡ fromℕ< n<o
-fromℕ<-cong m n r m<o n<o = fromℕ<′-cong {m} {n} ⦃ m<o ⦄ ⦃ n<o ⦄ r
+fromℕ<-cong 0       0                   _ _   _   = refl
+fromℕ<-cong (suc _) (suc _) {o = suc _} r m<n n<o
+  = cong suc (fromℕ<-cong _ _ (ℕₚ.suc-injective r) (ℕ.s<s⁻¹ m<n) (ℕ.s<s⁻¹ n<o))
 
-fromℕ<-injective : ∀ m n {o} (m<o : m ℕ.< o) (n<o : n ℕ.< o) →
-                   fromℕ< m<o ≡ fromℕ< n<o →
-                   m ≡ n
-fromℕ<-injective m n m<o n<o = fromℕ<′-injective ⦃ m<o ⦄ ⦃ n<o ⦄
-
--- fromℕ is a special case of fromℕ<.
-fromℕ-def : ∀ n → fromℕ n ≡ fromℕ< (ℕₚ.n<1+n n)
-fromℕ-def zero    = refl
-fromℕ-def (suc n) = cong suc (fromℕ-def n)
+fromℕ<-injective : ∀ m n {o} → .(m<o : m ℕ.< o) .(n<o : n ℕ.< o) →
+                   fromℕ< m<o ≡ fromℕ< n<o → m ≡ n
+fromℕ<-injective 0       0                   _   _   _  = refl
+fromℕ<-injective 0       (suc _) {o = suc _} _ _ ()
+fromℕ<-injective (suc _) (suc _) {o = suc _} m<n n<o r
+  = cong suc (fromℕ<-injective _ _ (ℕ.s<s⁻¹ m<n) (ℕ.s<s⁻¹ n<o) (suc-injective r))
 
 ------------------------------------------------------------------------
 -- fromℕ<″
 ------------------------------------------------------------------------
 
-fromℕ<″≡fromℕ : ∀ (m<″n : m ℕ.<″ n) →
-                let ℕ.less-than-or-equal {k} proof = m<″n
-                    instance _ = subst (ℕ.LessThan m) proof (ℕ.<″-lessThan {m} {k})
-                in
-                fromℕ<″ m m<″n ≡ fromℕLessThan m
-fromℕ<″≡fromℕ {m = zero}              (ℕ.<″-offset _) = refl
-fromℕ<″≡fromℕ {m = suc m} {n = suc n} (ℕ.<″-offset k) =
-  cong suc (fromℕ<″≡fromℕ (ℕ.<″-offset k))
-
-fromℕ<″≡fromℕ< : ∀ (m<″n : m ℕ.<″ n) →
-                 fromℕ<″ m m<″n ≡ fromℕ< (ℕₚ.≤″⇒≤ m<″n)
-fromℕ<″≡fromℕ< m<″n = fromℕ<″≡fromℕ m<″n
-
 fromℕ<≡fromℕ<″ : ∀ (m<n : m ℕ.< n) (m<″n : m ℕ.<″ n) →
                  fromℕ< m<n ≡ fromℕ<″ m m<″n
-fromℕ<≡fromℕ<″ _ m<″n = sym (fromℕ<″≡fromℕ< m<″n)
-
-toℕ-fromℕ<″ : ∀ (m<″n : m ℕ.<″ n) → toℕ (fromℕ<″ m m<″n) ≡ m
-toℕ-fromℕ<″ {m} {n} m<″n = begin
-  toℕ (fromℕ<″ m m<″n)        ≡⟨ cong toℕ (fromℕ<″≡fromℕ m<″n) ⟩
-  toℕ (fromℕLessThan m ⦃ _ ⦄) ≡⟨ toℕ-fromℕLessThan m ⦃ _ ⦄ ⟩
-  m                           ∎
+fromℕ<≡fromℕ<″ {m = zero}  m<n (ℕ.<″-offset _) = refl
+fromℕ<≡fromℕ<″ {m = suc m} m<n (ℕ.<″-offset _)
+  = cong suc (fromℕ<≡fromℕ<″ (ℕ.s<s⁻¹ m<n) (ℕ.<″-offset _))
+
+toℕ-fromℕ<″ : ∀ (m<n : m ℕ.<″ n) → toℕ (fromℕ<″ m m<n) ≡ m
+toℕ-fromℕ<″ {m} {n} m<n = begin
+  toℕ (fromℕ<″ m m<n)  ≡⟨ cong toℕ (sym (fromℕ<≡fromℕ<″ (ℕₚ.≤″⇒≤ m<n) m<n)) ⟩
+  toℕ (fromℕ< _)       ≡⟨ toℕ-fromℕ< (ℕₚ.≤″⇒≤ m<n) ⟩
+  m                    ∎
   where open ≡-Reasoning
 
 ------------------------------------------------------------------------
@@ -704,16 +615,10 @@ join-splitAt (suc m) n (suc i) = begin
 
 -- splitAt "m" "i" ≡ inj₁ "i" if i < m
 
-splitAt-LessThan : ∀ m {n} (i : Fin (m ℕ.+ n)) .⦃ lt : _ ⦄ →
-                   splitAt m i ≡ inj₁ (fromℕLessThan (toℕ i) ⦃ lt ⦄ )
-splitAt-LessThan (suc m) zero           = refl
-splitAt-LessThan (suc m) (suc i) =
-  cong (Sum.map suc id) (splitAt-LessThan m i)
-  where instance _ = ℕ.lessThanSucSuc
-
 splitAt-< : ∀ m {n} (i : Fin (m ℕ.+ n)) .(i<m : toℕ i ℕ.< m) →
             splitAt m i ≡ inj₁ (fromℕ< i<m)
-splitAt-< m i i<m = splitAt-LessThan m i ⦃ ℕ.<-lessThan i<m ⦄
+splitAt-< (suc m) zero    _   = refl
+splitAt-< (suc m) (suc i) i<m = cong (Sum.map suc id) (splitAt-< m i (ℕ.s<s⁻¹ i<m))
 
 -- splitAt "m" "i" ≡ inj₂ "i - m" if i ≥ m
 

From c8ecfd246065dfe4cb24649c7c7dc22a1ace08e8 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 29 Sep 2023 13:45:01 +0100
Subject: [PATCH 60/80] final tweaks to `CHANGELOG`

---
 CHANGELOG.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 314d8450d5..b2eaabaaec 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1365,8 +1365,8 @@ Deprecated names
 * In `Data.Nat.Properties`:
   ```
   suc[pred[n]]≡n  ↦  suc-pred
-  ≤-pred ↦ s≤s⁻¹
-  <-pred ↦ s<s⁻¹
+  ≤-pred          ↦  Data.Nat.Base.s≤s⁻¹
+  <-pred          ↦  Data.Nat.Base.s<s⁻¹
   ≤-step          ↦  m≤n⇒m≤1+n
   ≤-stepsˡ        ↦  m≤n⇒m≤o+n
   ≤-stepsʳ        ↦  m≤n⇒m≤n+o

From 547b416e425102f57a757362a67dcd49e5c5b5dc Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 4 Oct 2023 17:17:51 +0100
Subject: [PATCH 61/80] attempt to resolve the deprecation problem

---
 CHANGELOG.md                 |  5 +++--
 src/Data/Nat.agda            | 10 ++--------
 src/Data/Nat/Properties.agda | 13 ++++++++++---
 3 files changed, 15 insertions(+), 13 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index b2eaabaaec..3bf4a5d811 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2432,12 +2432,13 @@ Additions to existing modules
   m*n≢0     : .{{_ : NonZero m}} .{{_ : NonZero n}} → NonZero (m * n)
   m≤n⇒n∸m≤n : m ≤ n → n ∸ m ≤ n
 
-  ≤-pred        : suc m ≤ suc n → m ≤ n
   s<s-injective : ∀ {p q : m < n} → s<s p ≡ s<s q → p ≡ q
-  <-pred        : suc m < suc n → m < n
   <-step        : m < n → m < 1 + n
   m<1+n⇒m<n∨m≡n : m < suc n → m < n ⊎ m ≡ n
 
+  pred-mono-≤   : m ≤ n → pred m ≤ pred n
+  pred-mono-<   : .⦃ _ : NonZero m ⦄ → m < n → pred m < pred n
+
   z<′s : zero <′ suc n
   s<′s : m <′ n → suc m <′ suc n
   <⇒<′ : m < n → m <′ n
diff --git a/src/Data/Nat.agda b/src/Data/Nat.agda
index 1a4f06b475..503e32bac8 100644
--- a/src/Data/Nat.agda
+++ b/src/Data/Nat.agda
@@ -44,12 +44,6 @@ open import Data.Nat.Properties public
 
 -- Version 2.0
 
+-- solely for the sake of exposing the deprecation warnings for these two names
 open import Data.Nat.Properties public
-  hiding (≤-pred; <-pred)
-
-≤-pred : ∀ {m n} → (m ≤ n) → pred m ≤ pred n
-≤-pred {m = zero}              _   = z≤n
-≤-pred {m = suc _} {n = suc _} m≤n = s≤s⁻¹ m≤n
-
-<-pred : ∀ {m n} → .⦃ _ : NonZero m ⦄ → (m < n) → pred m < pred n
-<-pred {m = suc _} {n = suc _} = s<s⁻¹
+  using (≤-pred; <-pred)
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 8977a716ab..995de7f205 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -1697,6 +1697,13 @@ pred[n]≤n {suc n} = n≤1+n n
 suc-pred : ∀ n .{{_ : NonZero n}} → suc (pred n) ≡ n
 suc-pred (suc n) = refl
 
+pred-mono-≤ : ∀ {m n} → m ≤ n → pred m ≤ pred n
+pred-mono-≤ {m = zero}              _   = z≤n
+pred-mono-≤ {m = suc _} {n = suc _} m≤n = s≤s⁻¹ m≤n
+
+pred-mono-< : ∀ {m n} → .⦃ _ : NonZero m ⦄ → m < n → pred m < pred n
+pred-mono-< {m = suc _} {n = suc _} = s<s⁻¹
+
 ------------------------------------------------------------------------
 -- Properties of ∣_-_∣
 ------------------------------------------------------------------------
@@ -2295,12 +2302,12 @@ suc[pred[n]]≡n {suc n} _   = refl
 
 ≤-pred = s≤s⁻¹
 {-# WARNING_ON_USAGE ≤-pred
-"Warning: ≤-pred was deprecated in v2.0. Please use Data.Nat.Base.s≤s⁻¹  or Data.Nat.≤-pred instead. Note that the latter now has a different type. "
+"Warning: ≤-pred was deprecated in v2.0. Please use Data.Nat.Base.s≤s⁻¹  or pred-mono-≤ instead. Note that the latter now has a different type. "
 #-}
 
 <-pred = s<s⁻¹
-{-# WARNING_ON_USAGE ≤-pred
-"Warning: <-pred was deprecated in v2.0. Please use Data.Nat.Base.s<s⁻¹ or Data.Nat.<-pred instead. Note that the latter now has a different type using instance arguments."
+{-# WARNING_ON_USAGE <-pred
+"Warning: <-pred was deprecated in v2.0. Please use Data.Nat.Base.s<s⁻¹ or pred-mono-< instead. Note that the latter now has a different type using instance arguments."
 #-}
 
 ≤-step = m≤n⇒m≤1+n

From 4606f2ff221c78315c491382083d472eba30f286 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 4 Oct 2023 17:23:53 +0100
Subject: [PATCH 62/80] slight rearrangement ahead of attempt to resolve merge
 conflict

---
 CHANGELOG.md           |  3 +++
 src/Data/Nat/Base.agda | 10 +++++-----
 2 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3bf4a5d811..979e8c6699 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2381,6 +2381,9 @@ Additions to existing modules
   pattern <′-step {n} m<′n = ≤′-step {n} m<′n
 
   pattern ≤″-offset k = less-than-or-equal {k} refl
+  pattern <″-offset k = ≤″-offset k
+
+  s<″s⁻¹ : ∀ {m n} → suc m <″ suc n → m <″ n
 
   _⊔′_ : ℕ → ℕ → ℕ
   _⊓′_ : ℕ → ℕ → ℕ
diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda
index 01abccb8e1..59e805a4d1 100644
--- a/src/Data/Nat/Base.agda
+++ b/src/Data/Nat/Base.agda
@@ -279,11 +279,6 @@ record _≤″_ (m n : ℕ) : Set where
     {k}   : ℕ
     proof : m + k ≡ n
 
--- Smart constructor of _<″_
-
-pattern ≤″-offset k = less-than-or-equal {k = k} refl
-pattern <″-offset k = ≤″-offset k
-
 infix 4 _≤″_ _<″_ _≥″_ _>″_
 
 _<″_ : Rel ℕ 0ℓ
@@ -295,6 +290,11 @@ m ≥″ n = n ≤″ m
 _>″_ : Rel ℕ 0ℓ
 m >″ n = n <″ m
 
+-- Smart constructors of _≤″_ and _<″_
+
+pattern ≤″-offset k = less-than-or-equal {k = k} refl
+pattern <″-offset k = ≤″-offset k
+
 -- Smart destructor of _<″_
 
 s<″s⁻¹ : ∀ {m n} → suc m <″ suc n → m <″ n

From 7dd18ce05ec4f1734a69f3864f74caacc45102fb Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 4 Oct 2023 17:34:55 +0100
Subject: [PATCH 63/80] tweak

---
 src/Data/Fin/Base.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda
index ffe55a89b4..2c708a58c4 100644
--- a/src/Data/Fin/Base.agda
+++ b/src/Data/Fin/Base.agda
@@ -68,8 +68,8 @@ fromℕ (suc n) = suc (fromℕ n)
 -- fromℕ< {m} _ = "m".
 
 fromℕ< : ∀ {m n} → .(m ℕ.< n) → Fin n
-fromℕ< {zero}  {n = suc _} _   = zero
-fromℕ< {suc m} {n = suc _} m<n = suc (fromℕ< (ℕ.s<s⁻¹ m<n))
+fromℕ< {zero}  {suc _} _   = zero
+fromℕ< {suc m} {suc _} m<n = suc (fromℕ< (ℕ.s<s⁻¹ m<n))
 
 -- fromℕ<″ m _ = "m".
 

From 9ad32609b75bde581324a97c57ae28cd054305ef Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 4 Oct 2023 17:38:34 +0100
Subject: [PATCH 64/80] tweak `import`

---
 src/Data/Integer/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda
index 267047a13b..66f95807ba 100644
--- a/src/Data/Integer/Properties.agda
+++ b/src/Data/Integer/Properties.agda
@@ -16,7 +16,7 @@ import Algebra.Lattice.Construct.NaturalChoice.MinMaxOp as LatticeMinMaxOp
 import Algebra.Properties.AbelianGroup
 open import Data.Bool.Base using (T; true; false)
 open import Data.Integer.Base renaming (suc to sucℤ)
-open import Data.Nat as ℕ
+open import Data.Nat.Base as ℕ
   using (ℕ; suc; zero; _∸_; s≤s; z≤n; s<s; z<s; s≤s⁻¹; s<s⁻¹)
   hiding (module ℕ)
 import Data.Nat.Properties as ℕ

From fbd1c70aa341a51c335f01b7610162b80019d7b9 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 5 Oct 2023 06:39:30 +0100
Subject: [PATCH 65/80] =?UTF-8?q?BUG:=20strange=20reversion=20of=20`Data.F?=
 =?UTF-8?q?in.Properties.<-tri`:=20reappearance=20of=20deprecated=20`?=
 =?UTF-8?q?=E2=89=A4-pred`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Data/Fin/Properties.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index d38c53fc99..1d3bd1ef97 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -377,9 +377,9 @@ m <? n = suc (toℕ m) ℕₚ.≤? toℕ n
 <-cmp zero    (suc j) = tri< z<s   (λ()) (λ())
 <-cmp (suc i) zero    = tri> (λ()) (λ()) z<s
 <-cmp (suc i) (suc j) with <-cmp i j
-... | tri< i<j i≢j j≮i = tri< (s<s i<j)         (i≢j ∘ suc-injective) (j≮i ∘ ℕₚ.≤-pred)
-... | tri> i≮j i≢j j<i = tri> (i≮j ∘ ℕₚ.≤-pred) (i≢j ∘ suc-injective) (s<s j<i)
-... | tri≈ i≮j i≡j j≮i = tri≈ (i≮j ∘ ℕₚ.≤-pred) (cong suc i≡j)        (j≮i ∘ ℕₚ.≤-pred)
+... | tri< i<j i≢j j≮i = tri< (s<s i<j)     (i≢j ∘ suc-injective) (j≮i ∘ s<s⁻¹)
+... | tri> i≮j i≢j j<i = tri> (i≮j ∘ s<s⁻¹) (i≢j ∘ suc-injective) (s<s j<i)
+... | tri≈ i≮j i≡j j≮i = tri≈ (i≮j ∘ s<s⁻¹) (cong suc i≡j)        (j≮i ∘ ℕₚ.≤-pred)
 
 <-respˡ-≡ : (_<_ {m} {n}) Respectsˡ _≡_
 <-respˡ-≡ refl x≤y = x≤y

From 6954aa3ba2a45902cbb09d29d0a937046d5b8ba3 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 5 Oct 2023 06:43:53 +0100
Subject: [PATCH 66/80] =?UTF-8?q?BUG:=20strange=20reversion=20of=20`Data.F?=
 =?UTF-8?q?in.Properties.<-cmp`:=20reappearance=20of=20deprecated=20`?=
 =?UTF-8?q?=E2=89=A4-pred`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Data/Fin/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 1d3bd1ef97..0714907907 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -379,7 +379,7 @@ m <? n = suc (toℕ m) ℕₚ.≤? toℕ n
 <-cmp (suc i) (suc j) with <-cmp i j
 ... | tri< i<j i≢j j≮i = tri< (s<s i<j)     (i≢j ∘ suc-injective) (j≮i ∘ s<s⁻¹)
 ... | tri> i≮j i≢j j<i = tri> (i≮j ∘ s<s⁻¹) (i≢j ∘ suc-injective) (s<s j<i)
-... | tri≈ i≮j i≡j j≮i = tri≈ (i≮j ∘ s<s⁻¹) (cong suc i≡j)        (j≮i ∘ ℕₚ.≤-pred)
+... | tri≈ i≮j i≡j j≮i = tri≈ (i≮j ∘ s<s⁻¹) (cong suc i≡j)        (j≮i ∘ s<s⁻¹)
 
 <-respˡ-≡ : (_<_ {m} {n}) Respectsˡ _≡_
 <-respˡ-≡ refl x≤y = x≤y

From 0bafc6bd843217a6711e6794da2989eaff3a41cc Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 5 Oct 2023 06:47:35 +0100
Subject: [PATCH 67/80] =?UTF-8?q?fixed=20appearance=20of=20deprecated=20`?=
 =?UTF-8?q?=E2=89=A4-pred`=20in=20`Data.List.Properties`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Data/List/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 5afce0cd54..b037c7bb7a 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -850,7 +850,7 @@ drop-drop (suc m) n (x ∷ xs) = drop-drop m n xs
 
 drop-all : (n : ℕ) (xs : List A) → n ≥ length xs → drop n xs ≡ []
 drop-all n       []       _ = drop-[] n
-drop-all (suc n) (x ∷ xs) p = drop-all n xs (≤-pred p)
+drop-all (suc n) (x ∷ xs) p = drop-all n xs {!s≤s⁻¹ p!}
 
 ------------------------------------------------------------------------
 -- replicate

From ea0aba0b74220bfb5f15348cf17ece140dcf405b Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 5 Oct 2023 06:48:07 +0100
Subject: [PATCH 68/80] =?UTF-8?q?fixed=20appearance=20of=20deprecated=20`?=
 =?UTF-8?q?=E2=89=A4-pred`=20in=20`Data.List.Properties`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Data/List/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index b037c7bb7a..78fc03f865 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -850,7 +850,7 @@ drop-drop (suc m) n (x ∷ xs) = drop-drop m n xs
 
 drop-all : (n : ℕ) (xs : List A) → n ≥ length xs → drop n xs ≡ []
 drop-all n       []       _ = drop-[] n
-drop-all (suc n) (x ∷ xs) p = drop-all n xs {!s≤s⁻¹ p!}
+drop-all (suc n) (x ∷ xs) p = drop-all n xs (s≤s⁻¹ p)
 
 ------------------------------------------------------------------------
 -- replicate

From d901b5e587125077c7cee09b76da1237cc51aa00 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 6 Oct 2023 11:35:45 +0100
Subject: [PATCH 69/80] removed redundant `variable` quantified quantifier
 prefix

---
 src/Data/Fin/Base.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda
index 2c708a58c4..46db3b0910 100644
--- a/src/Data/Fin/Base.agda
+++ b/src/Data/Fin/Base.agda
@@ -67,7 +67,7 @@ fromℕ (suc n) = suc (fromℕ n)
 
 -- fromℕ< {m} _ = "m".
 
-fromℕ< : ∀ {m n} → .(m ℕ.< n) → Fin n
+fromℕ< : .(m ℕ.< n) → Fin n
 fromℕ< {zero}  {suc _} _   = zero
 fromℕ< {suc m} {suc _} m<n = suc (fromℕ< (ℕ.s<s⁻¹ m<n))
 

From 06fe00506c1684b73cf146417efaf7920335e5f9 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 6 Oct 2023 11:38:14 +0100
Subject: [PATCH 70/80] fixed `reduce`

---
 src/Data/Fin/Base.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda
index 46db3b0910..9b4c303f2f 100644
--- a/src/Data/Fin/Base.agda
+++ b/src/Data/Fin/Base.agda
@@ -93,9 +93,9 @@ zero    ↑ʳ i = i
 
 -- reduce≥ "m + i" _ = "i".
 
-reduce≥ : ∀ (i : Fin (m ℕ.+ n)) → .(m ℕ.≤ (toℕ i)) → Fin n
+reduce≥ : ∀ (i : Fin (m ℕ.+ n)) → .(m ℕ.≤ toℕ i) → Fin n
 reduce≥ {zero}  i       _   = i
-reduce≥ {suc m} (suc i) m≤i = reduce≥ {m} i (ℕ.s≤s⁻¹ m≤i)
+reduce≥ {suc _} (suc i) m≤i = reduce≥ i (ℕ.s≤s⁻¹ m≤i)
 
 -- inject⋆ m "i" = "i".
 

From 625f610b0b8941de59474237f200749a6ec1e8dc Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 6 Oct 2023 11:41:51 +0100
Subject: [PATCH 71/80] =?UTF-8?q?added=20`s=E2=89=A4=E2=80=B3s=E2=81=BB?=
 =?UTF-8?q?=C2=B9`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Data/Nat/Base.agda | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda
index 3bc7222fb1..9ab106194b 100644
--- a/src/Data/Nat/Base.agda
+++ b/src/Data/Nat/Base.agda
@@ -343,7 +343,10 @@ m >″ n = n <″ m
 pattern ≤″-offset k = less-than-or-equal {k = k} refl
 pattern <″-offset k = ≤″-offset k
 
--- Smart destructor of _<″_
+-- Smart destructors of _<″_
+
+s≤″s⁻¹ : ∀ {m n} → suc m ≤″ suc n → m ≤″ n
+s≤″s⁻¹ (≤″-offset k) = ≤″-offset k
 
 s<″s⁻¹ : ∀ {m n} → suc m <″ suc n → m <″ n
 s<″s⁻¹ (<″-offset k) = <″-offset k

From 65aa0ae2884de08b16fe107f3e7d4f6248ccd2ba Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 6 Oct 2023 11:43:10 +0100
Subject: [PATCH 72/80] =?UTF-8?q?added=20`s=E2=89=A4=E2=80=B3s=E2=81=BB?=
 =?UTF-8?q?=C2=B9`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CHANGELOG.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3e41ef98e1..7bee4ed85a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2590,6 +2590,7 @@ Additions to existing modules
   pattern ≤″-offset k = less-than-or-equal {k} refl
   pattern <″-offset k = ≤″-offset k
 
+  s≤″s⁻¹ : ∀ {m n} → suc m ≤″ suc n → m ≤″ n
   s<″s⁻¹ : ∀ {m n} → suc m <″ suc n → m <″ n
 
   _⊔′_ : ℕ → ℕ → ℕ

From 0de41987b13f19f8d3258e40fef035e5e46a67dc Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 6 Oct 2023 11:54:38 +0100
Subject: [PATCH 73/80] use of `Sum.map`

---
 src/Data/Nat/Properties.agda | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 26c50f78ef..bc17a94d3c 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -167,7 +167,7 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n))
 ≤-total : Total _≤_
 ≤-total zero    _       = inj₁ z≤n
 ≤-total _       zero    = inj₂ z≤n
-≤-total (suc m) (suc n) = [ inj₁ ∘ s≤s , inj₂ ∘ s≤s ]′ (≤-total m n)
+≤-total (suc m) (suc n) = Sum.map s≤s s≤s (≤-total m n)
 
 ≤-irrelevant : Irrelevant _≤_
 ≤-irrelevant z≤n        z≤n        = refl
@@ -453,8 +453,7 @@ m<n⇒m≤1+n = m≤n⇒m≤1+n ∘ <⇒≤
 m<1+n⇒m<n∨m≡n :  ∀ {m n} → m < suc n → m < n ⊎ m ≡ n
 m<1+n⇒m<n∨m≡n {0}     {0}     _           = inj₂ refl
 m<1+n⇒m<n∨m≡n {0}     {suc n} _           = inj₁ 0<1+n
-m<1+n⇒m<n∨m≡n {suc m} {suc n} (s<s m<1+n)
-  = [ inj₁ ∘ s<s , inj₂ ∘ (cong suc) ]′ (m<1+n⇒m<n∨m≡n m<1+n)
+m<1+n⇒m<n∨m≡n {suc m} {suc n} (s<s m<1+n) = Sum.map s<s (cong suc) (m<1+n⇒m<n∨m≡n m<1+n)
 
 m≤n⇒m<n∨m≡n :  ∀ {m n} → m ≤ n → m < n ⊎ m ≡ n
 m≤n⇒m<n∨m≡n m≤n = m<1+n⇒m<n∨m≡n (s≤s m≤n)

From b0c220fbada2b3c03406629e0396677ba84351c0 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 6 Oct 2023 12:05:46 +0100
Subject: [PATCH 74/80] rewrote header comments about alternative definitions
 of 'less than (or equal)'

---
 src/Data/Nat/Base.agda | 19 +++++++------------
 1 file changed, 7 insertions(+), 12 deletions(-)

diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda
index 9ab106194b..f2755c55fc 100644
--- a/src/Data/Nat/Base.agda
+++ b/src/Data/Nat/Base.agda
@@ -292,13 +292,10 @@ zero  ! = 1
 suc n ! = suc n * n !
 
 ------------------------------------------------------------------------
--- Alternative definitions of _≤_/_<_
+-- Extensionally equivalent alternative definitions of _≤_/_<_ etc.
 
-------------------------------------------------------------------------
--- An alternative definition of _≤_
-
--- The following definition of _≤_ is more suitable for well-founded
--- induction (see Data.Nat.Induction)
+-- _≤′_: this definition is more suitable for well-founded induction
+-- (see Data.Nat.Induction)
 
 infix 4 _≤′_ _<′_ _≥′_ _>′_
 
@@ -320,8 +317,9 @@ m ≥′ n = n ≤′ m
 _>′_ : Rel ℕ 0ℓ
 m >′ n = n <′ m
 
-------------------------------------------------------------------------
--- Another alternative definition of _≤_
+-- _≤″_: this definition of _≤_ is used for proof-irrelevant ‵DivMod`
+-- and is a specialised instance of a general algebraic construction
+
 infix 4 _≤″_ _<″_ _≥″_ _>″_
 
 _≤″_ : (m n : ℕ)  → Set
@@ -351,10 +349,7 @@ s≤″s⁻¹ (≤″-offset k) = ≤″-offset k
 s<″s⁻¹ : ∀ {m n} → suc m <″ suc n → m <″ n
 s<″s⁻¹ (<″-offset k) = <″-offset k
 
-------------------------------------------------------------------------
--- Another alternative definition of _≤_
-
--- Useful for induction when you have an upper bound.
+-- _≤‴_: this definition is useful for induction with an upper bound.
 
 data _≤‴_ : ℕ → ℕ → Set where
   ≤‴-refl : ∀{m} → m ≤‴ m

From 15b8f4196f393dbc6c9cdc33d601dd9cc3e9428f Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 6 Oct 2023 13:18:16 +0100
Subject: [PATCH 75/80] miscellaneous irrelevance simplifications, plus
 redundant parentheses

---
 src/Data/Fin/Properties.agda | 28 ++++++++++++++--------------
 1 file changed, 14 insertions(+), 14 deletions(-)

diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 0714907907..ea7c43c90f 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -535,33 +535,33 @@ inject₁≡⇒lower₁≡ n≢j i≡j = inject₁-injective (trans (inject₁-l
 ------------------------------------------------------------------------
 
 toℕ-inject≤ : ∀ i .(m≤n : m ℕ.≤ n) → toℕ (inject≤ i m≤n) ≡ toℕ i
-toℕ-inject≤ {_} {suc n} zero    _         = refl
-toℕ-inject≤ {_} {suc n} (suc i) m≤n = cong suc (toℕ-inject≤ i (ℕ.s≤s⁻¹ m≤n))
+toℕ-inject≤ {_} {suc n} zero    _ = refl
+toℕ-inject≤ {_} {suc n} (suc i) _ = cong suc (toℕ-inject≤ i _)
 
 inject≤-refl : ∀ i .(n≤n : n ℕ.≤ n) → inject≤ i n≤n ≡ i
 inject≤-refl {suc n} zero    _   = refl
-inject≤-refl {suc n} (suc i) n≤n = cong suc (inject≤-refl i (ℕ.s≤s⁻¹ n≤n))
+inject≤-refl {suc n} (suc i) _ = cong suc (inject≤-refl i _)
 
 inject≤-idempotent : ∀ (i : Fin m)
                      .(m≤n : m ℕ.≤ n) .(n≤o : n ℕ.≤ o) .(m≤o : m ℕ.≤ o) →
                      inject≤ (inject≤ i m≤n) n≤o ≡ inject≤ i m≤o
-inject≤-idempotent {_} {suc n} {suc o} zero    _   _   _   = refl
-inject≤-idempotent {_} {suc n} {suc o} (suc i) m≤n n≤o m≤o =
-  cong suc (inject≤-idempotent i (ℕ.s≤s⁻¹ m≤n) (ℕ.s≤s⁻¹ n≤o) (ℕ.s≤s⁻¹ m≤o))
+inject≤-idempotent {_} {suc n} {suc o} zero    _ _ _ = refl
+inject≤-idempotent {_} {suc n} {suc o} (suc i) _ _ _ =
+  cong suc (inject≤-idempotent i _ _ _)
 
-inject≤-trans : ∀ (i : Fin m) (m≤n : m ℕ.≤ n) (n≤o : n ℕ.≤ o) →
+inject≤-trans : ∀ (i : Fin m) .(m≤n : m ℕ.≤ n) .(n≤o : n ℕ.≤ o) →
                 inject≤ (inject≤ i m≤n) n≤o ≡ inject≤ i (ℕₚ.≤-trans m≤n n≤o)
-inject≤-trans i m≤n n≤o = inject≤-idempotent i m≤n n≤o _
+inject≤-trans i _ _ = inject≤-idempotent i _ _ _
 
 inject≤-injective : ∀ .(m≤n m≤n′ : m ℕ.≤ n) i j →
                     inject≤ i m≤n ≡ inject≤ j m≤n′ → i ≡ j
-inject≤-injective {n = suc _} p q zero    zero    eq = refl
-inject≤-injective {n = suc _} p q (suc i) (suc j) eq =
-  cong suc (inject≤-injective (ℕ.s≤s⁻¹ p) (ℕ.s≤s⁻¹ q) i j (suc-injective eq))
+inject≤-injective {n = suc _} _ _ zero    zero    eq = refl
+inject≤-injective {n = suc _} _ _ (suc i) (suc j) eq =
+  cong suc (inject≤-injective _ _ i j (suc-injective eq))
 
-inject≤-irrelevant : ∀ (m≤n m≤n′ : m ℕ.≤ n) i →
+inject≤-irrelevant : ∀ .(m≤n m≤n′ : m ℕ.≤ n) i →
                     inject≤ i m≤n ≡ inject≤ i m≤n′
-inject≤-irrelevant m≤n m≤n′ i = refl
+inject≤-irrelevant _ _ i = refl
 
 ------------------------------------------------------------------------
 -- pred
@@ -899,7 +899,7 @@ pinch-surjective (suc i) (suc j) = map suc (λ {f refl → cong suc (f refl)}) (
 
 pinch-mono-≤ : ∀ (i : Fin n) → (pinch i) Preserves _≤_ ⟶ _≤_
 pinch-mono-≤ 0F      {0F}    {k}     0≤n = z≤n
-pinch-mono-≤ 0F      {suc j} {suc k} j≤k = (ℕ.s≤s⁻¹ j≤k)
+pinch-mono-≤ 0F      {suc j} {suc k} j≤k = ℕ.s≤s⁻¹ j≤k
 pinch-mono-≤ (suc i) {0F}    {k}     0≤n = z≤n
 pinch-mono-≤ (suc i) {suc j} {suc k} j≤k = s≤s (pinch-mono-≤ i (ℕ.s≤s⁻¹ j≤k))
 

From b29679dc015779752563ee9cc599cf547af547fe Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 6 Oct 2023 13:45:05 +0100
Subject: [PATCH 76/80] resolved the deprecation conundrum

---
 src/Data/Nat.agda            |  4 ++--
 src/Data/Nat/Properties.agda | 14 ++++----------
 2 files changed, 6 insertions(+), 12 deletions(-)

diff --git a/src/Data/Nat.agda b/src/Data/Nat.agda
index 503e32bac8..8811565c11 100644
--- a/src/Data/Nat.agda
+++ b/src/Data/Nat.agda
@@ -44,6 +44,6 @@ open import Data.Nat.Properties public
 
 -- Version 2.0
 
--- solely for the sake of exposing the deprecation warnings for these two names
+-- solely for the re-export of this name, formerly in `Data.Nat.Properties.Core`
 open import Data.Nat.Properties public
-  using (≤-pred; <-pred)
+  using (≤-pred)
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index bc17a94d3c..f5301ff1d3 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -253,6 +253,8 @@ _≥?_ = flip _≤?_
 ------------------------------------------------------------------------
 -- Other properties of _≤_
 
+≤-pred = s≤s⁻¹
+
 s≤s-injective : ∀ {m n} {p q : m ≤ n} → s≤s p ≡ s≤s q → p ≡ q
 s≤s-injective refl = refl
 
@@ -279,6 +281,8 @@ n≤1⇒n≡0∨n≡1 (s≤s z≤n) = inj₂ refl
 
 -- Relationships between the various relations
 
+<-pred = s<s⁻¹
+
 <⇒≤ : _<_ ⇒ _≤_
 <⇒≤ z<s               = z≤n
 <⇒≤ (s<s m<n@(s≤s _)) = s≤s (<⇒≤ m<n)
@@ -2302,16 +2306,6 @@ suc[pred[n]]≡n {suc n} _   = refl
 "Warning: suc[pred[n]]≡n was deprecated in v2.0. Please use suc-pred instead. Note that the proof now uses instance arguments"
 #-}
 
-≤-pred = s≤s⁻¹
-{-# WARNING_ON_USAGE ≤-pred
-"Warning: ≤-pred was deprecated in v2.0. Please use Data.Nat.Base.s≤s⁻¹  or pred-mono-≤ instead. Note that the latter now has a different type. "
-#-}
-
-<-pred = s<s⁻¹
-{-# WARNING_ON_USAGE <-pred
-"Warning: <-pred was deprecated in v2.0. Please use Data.Nat.Base.s<s⁻¹ or pred-mono-< instead. Note that the latter now has a different type using instance arguments."
-#-}
-
 ≤-step = m≤n⇒m≤1+n
 {-# WARNING_ON_USAGE ≤-step
 "Warning: ≤-step was deprecated in v2.0. Please use m≤n⇒m≤1+n instead. "

From 729f45257b0850301c9759356c4e43068c9b0d72 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 6 Oct 2023 13:52:02 +0100
Subject: [PATCH 77/80] `lemma` is a terrible placeholder name; renamed

---
 src/Data/Nat/DivMod.agda | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda
index 29f65b837a..64b7bedd37 100644
--- a/src/Data/Nat/DivMod.agda
+++ b/src/Data/Nat/DivMod.agda
@@ -467,7 +467,7 @@ m mod n = fromℕ< (m%n<n m n)
 _divMod_ : (dividend divisor : ℕ) .{{_ : NonZero divisor}} →
            DivMod dividend divisor
 m divMod n = result (m / n) (m mod n) $ begin-equality
-  m                             ≡⟨  m≡m%n+[m/n]*n m n ⟩
-  m % n              + [m/n]*n  ≡˘⟨ cong (_+ [m/n]*n) (toℕ-fromℕ< lemma) ⟩
-  toℕ (fromℕ< lemma) + [m/n]*n  ∎
-  where [m/n]*n = m / n * n ; lemma = m%n<n m n
+  m                               ≡⟨  m≡m%n+[m/n]*n m n ⟩
+  m % n                + [m/n]*n  ≡˘⟨ cong (_+ [m/n]*n) (toℕ-fromℕ< [m%n]<n) ⟩
+  toℕ (fromℕ< [m%n]<n) + [m/n]*n  ∎
+  where [m/n]*n = m / n * n ; [m%n]<n = m%n<n m n

From 60917a6deb46be7a428305f965fe673aaed306b2 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 6 Oct 2023 13:55:41 +0100
Subject: [PATCH 78/80] relocations

---
 src/Data/Nat/Properties.agda | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index f5301ff1d3..8a7201c6fe 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -253,11 +253,11 @@ _≥?_ = flip _≤?_
 ------------------------------------------------------------------------
 -- Other properties of _≤_
 
-≤-pred = s≤s⁻¹
-
 s≤s-injective : ∀ {m n} {p q : m ≤ n} → s≤s p ≡ s≤s q → p ≡ q
 s≤s-injective refl = refl
 
+≤-pred = s≤s⁻¹
+
 m≤n⇒m≤1+n : ∀ {m n} → m ≤ n → m ≤ 1 + n
 m≤n⇒m≤1+n z≤n       = z≤n
 m≤n⇒m≤1+n (s≤s m≤n) = s≤s (m≤n⇒m≤1+n m≤n)
@@ -281,8 +281,6 @@ n≤1⇒n≡0∨n≡1 (s≤s z≤n) = inj₂ refl
 
 -- Relationships between the various relations
 
-<-pred = s<s⁻¹
-
 <⇒≤ : _<_ ⇒ _≤_
 <⇒≤ z<s               = z≤n
 <⇒≤ (s<s m<n@(s≤s _)) = s≤s (<⇒≤ m<n)
@@ -419,6 +417,8 @@ _>?_ = flip _<?_
 s<s-injective : ∀ {m n} {p q : m < n} → s<s p ≡ s<s q → p ≡ q
 s<s-injective refl = refl
 
+<-pred = s<s⁻¹
+
 m<n⇒m<1+n : ∀ {m n} → m < n → m < 1 + n
 m<n⇒m<1+n z<s               = z<s
 m<n⇒m<1+n (s<s m<n@(s≤s _)) = s<s (m<n⇒m<1+n m<n)

From e9c9f44c73ece9c87436aa972b284f0d9093fe4a Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 6 Oct 2023 14:38:57 +0100
Subject: [PATCH 79/80] deprecated `pred-mono`

---
 CHANGELOG.md                 |  3 +--
 src/Data/Nat/Properties.agda | 14 ++++++++------
 2 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 7bee4ed85a..4a5515b4dc 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1517,12 +1517,11 @@ Deprecated names
 * In `Data.Nat.Properties`:
   ```
   suc[pred[n]]≡n  ↦  suc-pred
-  ≤-pred          ↦  Data.Nat.Base.s≤s⁻¹
-  <-pred          ↦  Data.Nat.Base.s<s⁻¹
   ≤-step          ↦  m≤n⇒m≤1+n
   ≤-stepsˡ        ↦  m≤n⇒m≤o+n
   ≤-stepsʳ        ↦  m≤n⇒m≤n+o
   <-step          ↦  m<n⇒m<1+n
+  pred-mono       ↦  pred-mono-≤
   ```
 
 * In `Data.Rational.Unnormalised.Base`:
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 8a7201c6fe..9b17aae0c7 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -1679,9 +1679,6 @@ m⊓n+n∸m≡n (suc m) (suc n) = cong suc $ m⊓n+n∸m≡n m n
 -- Properties of pred
 ------------------------------------------------------------------------
 
-pred-mono : pred Preserves _≤_ ⟶ _≤_
-pred-mono m≤n = ∸-mono m≤n (≤-refl {1})
-
 pred[n]≤n : ∀ {n} → pred n ≤ n
 pred[n]≤n {zero}  = z≤n
 pred[n]≤n {suc n} = n≤1+n n
@@ -1700,9 +1697,9 @@ pred[n]≤n {suc n} = n≤1+n n
 suc-pred : ∀ n .{{_ : NonZero n}} → suc (pred n) ≡ n
 suc-pred (suc n) = refl
 
-pred-mono-≤ : ∀ {m n} → m ≤ n → pred m ≤ pred n
-pred-mono-≤ {m = zero}              _   = z≤n
-pred-mono-≤ {m = suc _} {n = suc _} m≤n = s≤s⁻¹ m≤n
+pred-mono-≤ : pred Preserves _≤_ ⟶ _≤_
+pred-mono-≤ {zero}          _   = z≤n
+pred-mono-≤ {suc _} {suc _} m≤n = s≤s⁻¹ m≤n
 
 pred-mono-< : ∀ {m n} → .⦃ _ : NonZero m ⦄ → m < n → pred m < pred n
 pred-mono-< {m = suc _} {n = suc _} = s<s⁻¹
@@ -2326,6 +2323,11 @@ suc[pred[n]]≡n {suc n} _   = refl
 "Warning: <-step was deprecated in v2.0. Please use m<n⇒m<1+n instead. "
 #-}
 
+pred-mono = pred-mono-≤
+{-# WARNING_ON_USAGE pred-mono
+"Warning: pred-mono was deprecated in v2.0. Please use pred-mono-≤ instead. "
+#-}
+
 {- issue1844/issue1755: raw bundles have moved to `Data.X.Base` -}
 open Data.Nat.Base public
   using (*-rawMagma; *-1-rawMonoid)

From 308c9906d94ea6901801137e36e6486198b52b6a Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 6 Oct 2023 18:03:47 +0100
Subject: [PATCH 80/80] fixed deprecation error

---
 src/Data/Nat/Binary/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda
index a479afdfa8..6109106b26 100644
--- a/src/Data/Nat/Binary/Properties.agda
+++ b/src/Data/Nat/Binary/Properties.agda
@@ -1459,7 +1459,7 @@ pred-mono-≤ : pred Preserves _≤_ ⟶ _≤_
 pred-mono-≤ {x} {y} x≤y = begin
   pred x             ≡⟨ cong pred (sym (fromℕ-toℕ x)) ⟩
   pred (fromℕ m)     ≡⟨ sym (fromℕ-pred m) ⟩
-  fromℕ (ℕ.pred m)   ≤⟨ fromℕ-mono-≤ (ℕₚ.pred-mono (toℕ-mono-≤ x≤y)) ⟩
+  fromℕ (ℕ.pred m)   ≤⟨ fromℕ-mono-≤ (ℕₚ.pred-mono-≤ (toℕ-mono-≤ x≤y)) ⟩
   fromℕ (ℕ.pred n)   ≡⟨ fromℕ-pred n ⟩
   pred (fromℕ n)     ≡⟨ cong pred (fromℕ-toℕ y) ⟩
   pred y             ∎