From 4701dc59822ca3c8b92bfea3752c2ddc81b1c051 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 27 Mar 2026 18:18:45 +0000
Subject: [PATCH 01/15] [ add ] proof of Carette's Lemma

---
 CHANGELOG.md             | 12 ++++++
 src/Data/Nat/DivMod.agda | 80 +++++++++++++++++++++++++++++++++++++++-
 2 files changed, 91 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 99dea4e749..65d191cee7 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -319,6 +319,18 @@ Additions to existing modules
   n≤o⇒m^n∣m^o : ∀ m → .(n ≤ o) → m ^ n ∣ m ^ o
   ```
 
+* In `Data.Nat.DivMod`:
+  ```agda
+  infix 4 _≲%[_]_ _≡%[_]_ : ∀ m o n → Set _
+  m ≲%[ o ] n = ∃ λ k → n ≡ m + k * o
+  m ≡%[ o ] n = SymClosure _≲%[ o ]_ m n
+  ≲%[o]-suc   : m ≲%[ o ] n → (suc m) ≲%[ o ] (suc n)
+  ≲%[o]-suc⁻¹ : (suc m) ≲%[ o ] (suc n) → m ≲%[ o ] n
+  ≲%[o]⇒%o≡%o : .{{_ : NonZero o}} → m ≲%[ o ] n → m % o ≡ n % o
+  %o≡%o⇒≲%[o] : .{{_ : NonZero o}} → m % o ≡ n % o → m ≤ n → m ≲%[ o ] n
+  %o≡%o⇒≡%[o] : .{{_ : NonZero o}} → m % o ≡ n % o → m ≡%[ o ] n
+  ```
+
 * In `Data.Nat.Logarithm`
   ```agda
   2^⌊log₂n⌋≤n : ∀ n .{{ _ : NonZero n }} → 2 ^ ⌊log₂ n ⌋ ≤ n
diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda
index 86bc8d3168..f8351bc5f9 100644
--- a/src/Data/Nat/DivMod.agda
+++ b/src/Data/Nat/DivMod.agda
@@ -17,9 +17,11 @@ open import Data.Nat.DivMod.Core
 open import Data.Nat.Divisibility.Core
 open import Data.Nat.Induction
 open import Data.Nat.Properties
-open import Data.Product.Base using (_,_)
+open import Data.Product.Base using (_,_; ∃)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Function.Base using (_$_; _∘_)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Construct.Closure.Symmetric
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; cong; cong₂; refl; trans; _≢_; sym)
 open import Relation.Nullary.Negation using (contradiction)
@@ -463,6 +465,82 @@ m%n*o≡m*o%[n*o] m n o = begin-equality
     p-1 * n + n ≡⟨ +-comm (p-1 * n) n ⟩
     pn          ∎
 
+-- Lemmas characterising `m ≡ n (mod o)`
+
+-- Definition of an asymmetric version of that notion
+-- NB. `Relation.Binary.Construct.Closure.Symmetric`
+-- gives us the relation we're after.
+
+infix 4 _≲%[_]_ _≡%[_]_
+_≲%[_]_ _≡%[_]_ : ∀ m o n → Set _
+
+m ≲%[ o ] n = ∃ λ k → n ≡ m + k * o
+m ≡%[ o ] n = SymClosure _≲%[ o ]_ m n
+
+-- simple properties wrt successor
+
+≲%[o]-suc : m ≲%[ o ] n → (suc m) ≲%[ o ] (suc n)
+≲%[o]-suc (k , eq) = k , cong suc eq
+
+≲%[o]-suc⁻¹ : (suc m) ≲%[ o ] (suc n) → m ≲%[ o ] n
+≲%[o]-suc⁻¹ (k , eq) = k , cong pred eq
+
+-- Equivalence with the relation we seek to characterise
+
+module _ .{{_ : NonZero o}} where
+
+  ≲%[o]⇒%o≡%o : m ≲%[ o ] n → m % o ≡ n % o
+  ≲%[o]⇒%o≡%o {m = m} {n = n} (k , eq) = begin-equality
+    m % o           ≡⟨ [m+kn]%n≡m%n m k o ⟨
+    (m + k * o) % o ≡⟨ cong (_% o) eq ⟨
+    n % o ∎
+
+  %o≡%o⇒≲%[o] : m % o ≡ n % o → m ≤ n → m ≲%[ o ] n
+  %o≡%o⇒≲%[o] {m = m} {n = n} eq m≤n = k , (begin-equality
+    n                           ≡⟨ m≡m%n+[m/n]*n n o ⟩
+    n % o + n / o * o           ≡⟨ cong (_+ n / o * o) eq ⟨
+    m % o + n / o * o           ≡⟨ cong ((m % o +_) ∘ (_* o)) (m+[n∸m]≡n (/-monoˡ-≤ o m≤n)) ⟨
+    m % o + (m / o + k) * o     ≡⟨ cong (m % o +_) (*-distribʳ-+ o (m / o) k) ⟩
+    m % o + (m / o * o + k * o) ≡⟨ +-assoc (m % o) _ _ ⟨
+    (m % o + m / o * o) + k * o ≡⟨ cong (_+ k * o) (m≡m%n+[m/n]*n m o) ⟨
+    m + k * o                   ∎)
+    where k = n / o ∸ m / o
+
+  %o≡%o⇒≡%[o] : m % o ≡ n % o → m ≡%[ o ] n
+  %o≡%o⇒≡%[o] {m = m} {n = n} eq with ≤-total m n
+  ... | inj₁ m≤n = fwd (%o≡%o⇒≲%[o] eq m≤n)
+  ... | inj₂ n≤m = bwd (%o≡%o⇒≲%[o] (sym eq) n≤m)
+
+
+private
+
+  -- Example application, a result sought by Jacques Carette, taken from
+  -- https://agda.zulipchat.com/#narrow/channel/264623-stdlib/topic/suc.20injective.20under.20_.25_/with/582024092
+
+  CarettesLemma : ∀ o .{{_ : NonZero o}} → Rel ℕ _
+  CarettesLemma o m n = (suc m) % o ≡ (suc n) % o → m % o ≡ n % o
+
+  carettesLemma : .{{_ : NonZero o}} → CarettesLemma o m n
+  carettesLemma eq with %o≡%o⇒≡%[o] eq
+  ... | fwd m≲n = ≲%[o]⇒%o≡%o (≲%[o]-suc⁻¹ m≲n)
+  ... | bwd n≲m = sym (≲%[o]⇒%o≡%o (≲%[o]-suc⁻¹ n≲m))
+
+  -- Alex Rice's optimised proof
+  carettesLemma′ : .{{_ : NonZero o}} → CarettesLemma o m n
+  carettesLemma′ {o = o@(suc d)} {m = m} {n = n} eq = begin-equality
+    m % o                       ≡⟨ lemma m ⟩
+    (suc m % o + d % o) % suc d ≡⟨ cong (λ a → (a + d % suc d) % suc d) eq ⟩
+    (suc n % o + d % o) % suc d ≡⟨ lemma n ⟨
+    n % o ∎
+    where
+    lemma : ∀ n → n % o ≡ (suc n % o + d % o) % o
+    lemma n = begin-equality
+      n % o                   ≡⟨ [m+n]%n≡m%n n o ⟨
+      (n + suc d) % o         ≡⟨ %-congˡ (+-suc n d) ⟩
+      (suc n + d) % o         ≡⟨ %-distribˡ-+ (suc n) d o ⟩
+      (suc n % o + d % o) % o ∎
+
+
 ------------------------------------------------------------------------
 --  A specification of integer division.
 

From c9ca2f067acbee93aa4222924f80c45b9d8c6c6c Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 27 Mar 2026 20:57:10 +0000
Subject: [PATCH 02/15] refactor: remove simple lemmas

---
 src/Data/Nat/DivMod.agda | 14 +++-----------
 1 file changed, 3 insertions(+), 11 deletions(-)

diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda
index f8351bc5f9..7dbd9c1c10 100644
--- a/src/Data/Nat/DivMod.agda
+++ b/src/Data/Nat/DivMod.agda
@@ -21,7 +21,7 @@ open import Data.Product.Base using (_,_; ∃)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Function.Base using (_$_; _∘_)
 open import Relation.Binary.Core using (Rel)
-open import Relation.Binary.Construct.Closure.Symmetric
+open import Relation.Binary.Construct.Closure.Symmetric as SymClosure
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; cong; cong₂; refl; trans; _≢_; sym)
 open import Relation.Nullary.Negation using (contradiction)
@@ -477,14 +477,6 @@ _≲%[_]_ _≡%[_]_ : ∀ m o n → Set _
 m ≲%[ o ] n = ∃ λ k → n ≡ m + k * o
 m ≡%[ o ] n = SymClosure _≲%[ o ]_ m n
 
--- simple properties wrt successor
-
-≲%[o]-suc : m ≲%[ o ] n → (suc m) ≲%[ o ] (suc n)
-≲%[o]-suc (k , eq) = k , cong suc eq
-
-≲%[o]-suc⁻¹ : (suc m) ≲%[ o ] (suc n) → m ≲%[ o ] n
-≲%[o]-suc⁻¹ (k , eq) = k , cong pred eq
-
 -- Equivalence with the relation we seek to characterise
 
 module _ .{{_ : NonZero o}} where
@@ -522,8 +514,8 @@ private
 
   carettesLemma : .{{_ : NonZero o}} → CarettesLemma o m n
   carettesLemma eq with %o≡%o⇒≡%[o] eq
-  ... | fwd m≲n = ≲%[o]⇒%o≡%o (≲%[o]-suc⁻¹ m≲n)
-  ... | bwd n≲m = sym (≲%[o]⇒%o≡%o (≲%[o]-suc⁻¹ n≲m))
+  ... | fwd (k , eq) = ≲%[o]⇒%o≡%o (k , cong pred eq)
+  ... | bwd (k , eq) = sym (≲%[o]⇒%o≡%o (k , cong pred eq))
 
   -- Alex Rice's optimised proof
   carettesLemma′ : .{{_ : NonZero o}} → CarettesLemma o m n

From 0ce7a21ee9ddee70fcf9f148352068cf7093d157 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 28 Mar 2026 08:46:20 +0000
Subject: [PATCH 03/15] add: one half of the equivalence

---
 CHANGELOG.md             | 1 +
 src/Data/Nat/DivMod.agda | 6 +++++-
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 65d191cee7..1dcef5ff4d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -327,6 +327,7 @@ Additions to existing modules
   ≲%[o]-suc   : m ≲%[ o ] n → (suc m) ≲%[ o ] (suc n)
   ≲%[o]-suc⁻¹ : (suc m) ≲%[ o ] (suc n) → m ≲%[ o ] n
   ≲%[o]⇒%o≡%o : .{{_ : NonZero o}} → m ≲%[ o ] n → m % o ≡ n % o
+  ≡%[o]⇒%o≡%o : .{{_ : NonZero o}} → m ≡%[ o ] n → m % o ≡ n % o
   %o≡%o⇒≲%[o] : .{{_ : NonZero o}} → m % o ≡ n % o → m ≤ n → m ≲%[ o ] n
   %o≡%o⇒≡%[o] : .{{_ : NonZero o}} → m % o ≡ n % o → m ≡%[ o ] n
   ```
diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda
index 7dbd9c1c10..eac727897b 100644
--- a/src/Data/Nat/DivMod.agda
+++ b/src/Data/Nat/DivMod.agda
@@ -21,7 +21,8 @@ open import Data.Product.Base using (_,_; ∃)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Function.Base using (_$_; _∘_)
 open import Relation.Binary.Core using (Rel)
-open import Relation.Binary.Construct.Closure.Symmetric as SymClosure
+open import Relation.Binary.Construct.Closure.Symmetric
+  as SymClosure using (SymClosure; fwd; bwd)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; cong; cong₂; refl; trans; _≢_; sym)
 open import Relation.Nullary.Negation using (contradiction)
@@ -487,6 +488,9 @@ module _ .{{_ : NonZero o}} where
     (m + k * o) % o ≡⟨ cong (_% o) eq ⟨
     n % o ∎
 
+  ≡%[o]⇒%o≡%o : m ≡%[ o ] n → m % o ≡ n % o
+  ≡%[o]⇒%o≡%o {m = m} {n = n} = SymClosure.fold sym ≲%[o]⇒%o≡%o
+
   %o≡%o⇒≲%[o] : m % o ≡ n % o → m ≤ n → m ≲%[ o ] n
   %o≡%o⇒≲%[o] {m = m} {n = n} eq m≤n = k , (begin-equality
     n                           ≡⟨ m≡m%n+[m/n]*n n o ⟩

From 6752397f70b91c194f5a721bd2b1231ee6f1a183 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 29 Mar 2026 12:31:44 +0100
Subject: [PATCH 04/15] =?UTF-8?q?refactor:=20in=20terms=20of=20`=5Fon=5F`?=
 =?UTF-8?q?=20and=20`=5F=E2=87=92=5F`;=20introduce=20name=20for=20equality?=
 =?UTF-8?q?=20mod=20`o`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CHANGELOG.md             | 14 +++++-----
 src/Data/Nat/DivMod.agda | 56 +++++++++++++++++++++++-----------------
 2 files changed, 40 insertions(+), 30 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1dcef5ff4d..539955ac4d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -324,12 +324,14 @@ Additions to existing modules
   infix 4 _≲%[_]_ _≡%[_]_ : ∀ m o n → Set _
   m ≲%[ o ] n = ∃ λ k → n ≡ m + k * o
   m ≡%[ o ] n = SymClosure _≲%[ o ]_ m n
-  ≲%[o]-suc   : m ≲%[ o ] n → (suc m) ≲%[ o ] (suc n)
-  ≲%[o]-suc⁻¹ : (suc m) ≲%[ o ] (suc n) → m ≲%[ o ] n
-  ≲%[o]⇒%o≡%o : .{{_ : NonZero o}} → m ≲%[ o ] n → m % o ≡ n % o
-  ≡%[o]⇒%o≡%o : .{{_ : NonZero o}} → m ≡%[ o ] n → m % o ≡ n % o
-  %o≡%o⇒≲%[o] : .{{_ : NonZero o}} → m % o ≡ n % o → m ≤ n → m ≲%[ o ] n
-  %o≡%o⇒≡%[o] : .{{_ : NonZero o}} → m % o ≡ n % o → m ≡%[ o ] n
+
+  infix 4 _≡[_]%_ : ∀ m o .{{_ : NonZero o}} n → Set _
+  m ≡[ o ]% n = m % o ≡ n % o
+
+  ≲%[o]⇒≡[o]% : .{{_ : NonZero o}} → _≲%[ o ]_ ⇒ _≡[ o ]%_
+  ≡%[o]⇒≡[o]% : .{{_ : NonZero o}} → _≡%[ o ]_ ⇒ _≡[ o ]%_
+  ≡[o]%⇒≲%[o] : .{{_ : NonZero o}} → m % o ≡ n % o → m ≤ n → m ≲%[ o ] n
+  ≡[o]%⇒≡%[o] : .{{_ : NonZero o}} → _≡[ o ]%_ ⇒ _≡%[ o ]_
   ```
 
 * In `Data.Nat.Logarithm`
diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda
index eac727897b..fcc2695cf1 100644
--- a/src/Data/Nat/DivMod.agda
+++ b/src/Data/Nat/DivMod.agda
@@ -19,8 +19,8 @@ open import Data.Nat.Induction
 open import Data.Nat.Properties
 open import Data.Product.Base using (_,_; ∃)
 open import Data.Sum.Base using (inj₁; inj₂)
-open import Function.Base using (_$_; _∘_)
-open import Relation.Binary.Core using (Rel)
+open import Function.Base using (_$_; _∘_; _on_)
+open import Relation.Binary.Core using (Rel; _⇒_)
 open import Relation.Binary.Construct.Closure.Symmetric
   as SymClosure using (SymClosure; fwd; bwd)
 open import Relation.Binary.PropositionalEquality.Core
@@ -478,21 +478,25 @@ _≲%[_]_ _≡%[_]_ : ∀ m o n → Set _
 m ≲%[ o ] n = ∃ λ k → n ≡ m + k * o
 m ≡%[ o ] n = SymClosure _≲%[ o ]_ m n
 
--- Equivalence with the relation we seek to characterise
+infix 4 _≡[_]%_
+_≡[_]%_ : ∀ m o .{{_ : NonZero o}} n → Set _
+m ≡[ o ]% n = m % o ≡ n % o
+
+-- Equivalence between _≡%[_]_ and _≡[_]%_
 
 module _ .{{_ : NonZero o}} where
 
-  ≲%[o]⇒%o≡%o : m ≲%[ o ] n → m % o ≡ n % o
-  ≲%[o]⇒%o≡%o {m = m} {n = n} (k , eq) = begin-equality
+  ≲%[o]⇒≡[o]% : _≲%[ o ]_ ⇒ _≡[ o ]%_
+  ≲%[o]⇒≡[o]% {x = m} {y = n} (k , eq) = begin-equality
     m % o           ≡⟨ [m+kn]%n≡m%n m k o ⟨
     (m + k * o) % o ≡⟨ cong (_% o) eq ⟨
     n % o ∎
 
-  ≡%[o]⇒%o≡%o : m ≡%[ o ] n → m % o ≡ n % o
-  ≡%[o]⇒%o≡%o {m = m} {n = n} = SymClosure.fold sym ≲%[o]⇒%o≡%o
+  ≡%[o]⇒≡[o]% : _≡%[ o ]_ ⇒ _≡[ o ]%_
+  ≡%[o]⇒≡[o]% = SymClosure.fold sym ≲%[o]⇒≡[o]%
 
-  %o≡%o⇒≲%[o] : m % o ≡ n % o → m ≤ n → m ≲%[ o ] n
-  %o≡%o⇒≲%[o] {m = m} {n = n} eq m≤n = k , (begin-equality
+  ≡[o]%⇒≲%[o] : m % o ≡ n % o → m ≤ n → m ≲%[ o ] n
+  ≡[o]%⇒≲%[o] {m = m} {n = n} eq m≤n = k , (begin-equality
     n                           ≡⟨ m≡m%n+[m/n]*n n o ⟩
     n % o + n / o * o           ≡⟨ cong (_+ n / o * o) eq ⟨
     m % o + n / o * o           ≡⟨ cong ((m % o +_) ∘ (_* o)) (m+[n∸m]≡n (/-monoˡ-≤ o m≤n)) ⟨
@@ -502,10 +506,10 @@ module _ .{{_ : NonZero o}} where
     m + k * o                   ∎)
     where k = n / o ∸ m / o
 
-  %o≡%o⇒≡%[o] : m % o ≡ n % o → m ≡%[ o ] n
-  %o≡%o⇒≡%[o] {m = m} {n = n} eq with ≤-total m n
-  ... | inj₁ m≤n = fwd (%o≡%o⇒≲%[o] eq m≤n)
-  ... | inj₂ n≤m = bwd (%o≡%o⇒≲%[o] (sym eq) n≤m)
+  ≡[o]%⇒≡%[o] : _≡[ o ]%_ ⇒ _≡%[ o ]_
+  ≡[o]%⇒≡%[o] {x = m} {y = n} eq with ≤-total m n
+  ... | inj₁ m≤n = fwd (≡[o]%⇒≲%[o] eq m≤n)
+  ... | inj₂ n≤m = bwd (≡[o]%⇒≲%[o] (sym eq) n≤m)
 
 
 private
@@ -513,25 +517,29 @@ private
   -- Example application, a result sought by Jacques Carette, taken from
   -- https://agda.zulipchat.com/#narrow/channel/264623-stdlib/topic/suc.20injective.20under.20_.25_/with/582024092
 
-  CarettesLemma : ∀ o .{{_ : NonZero o}} → Rel ℕ _
-  CarettesLemma o m n = (suc m) % o ≡ (suc n) % o → m % o ≡ n % o
+  ≲%[o]-suc⁻¹ : (_≲%[ o ]_ on suc) ⇒ _≲%[ o ]_
+  ≲%[o]-suc⁻¹ (k , eq) = k , cong pred eq
+
+  CarettesLemma : ∀ o .{{_ : NonZero o}} → Set _
+  CarettesLemma o = (_≡[ o ]%_ on suc) ⇒ _≡[ o ]%_
 
-  carettesLemma : .{{_ : NonZero o}} → CarettesLemma o m n
-  carettesLemma eq with %o≡%o⇒≡%[o] eq
-  ... | fwd (k , eq) = ≲%[o]⇒%o≡%o (k , cong pred eq)
-  ... | bwd (k , eq) = sym (≲%[o]⇒%o≡%o (k , cong pred eq))
+  carettesLemma : .{{_ : NonZero o}} → CarettesLemma o
+  carettesLemma eq with ≡[o]%⇒≡%[o] eq
+  ... | fwd m≲n = ≲%[o]⇒≡[o]% (≲%[o]-suc⁻¹ m≲n)
+  ... | bwd n≲m = sym (≲%[o]⇒≡[o]% (≲%[o]-suc⁻¹ n≲m))
 
   -- Alex Rice's optimised proof
-  carettesLemma′ : .{{_ : NonZero o}} → CarettesLemma o m n
-  carettesLemma′ {o = o@(suc d)} {m = m} {n = n} eq = begin-equality
-    m % o                       ≡⟨ lemma m ⟩
-    (suc m % o + d % o) % suc d ≡⟨ cong (λ a → (a + d % suc d) % suc d) eq ⟩
-    (suc n % o + d % o) % suc d ≡⟨ lemma n ⟨
+  carettesLemma′ : .{{_ : NonZero o}} → CarettesLemma o
+  carettesLemma′ {o = o@(suc d)} {x = m} {y = n} eq = begin-equality
+    m % o                   ≡⟨ lemma m ⟩
+    (suc m % o + d % o) % o ≡⟨ cong (λ a → (a + d % o) % o) eq ⟩
+    (suc n % o + d % o) % o ≡⟨ lemma n ⟨
     n % o ∎
     where
     lemma : ∀ n → n % o ≡ (suc n % o + d % o) % o
     lemma n = begin-equality
       n % o                   ≡⟨ [m+n]%n≡m%n n o ⟨
+      (n + o) % o             ≡⟨⟩
       (n + suc d) % o         ≡⟨ %-congˡ (+-suc n d) ⟩
       (suc n + d) % o         ≡⟨ %-distribˡ-+ (suc n) d o ⟩
       (suc n % o + d % o) % o ∎

From 48310dbc981a7b4cb66e59f749fe065cfc846568 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 30 Mar 2026 08:57:30 +0100
Subject: [PATCH 05/15] add: new lemmas relating `SymClosure` and `on`

---
 CHANGELOG.md                                  |  8 ++++++++
 .../Binary/Construct/Closure/Symmetric.agda   | 20 +++++++++++++++----
 2 files changed, 24 insertions(+), 4 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 539955ac4d..ca02a2b1e8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -496,6 +496,14 @@ Additions to existing modules
   ≤⁺-resp-≈⁺ : _≤_ Respects₂ _≈_ → _≤⁺_ Respects₂ _≈⁺_
   ```
 
+* In `Relation.Binary.Construct.Closure.Symmetric`:
+  ```
+  hmap : ∀ (g : C → A) (f : C → B) → (R on g) ⇒ (S on f) →
+         ((SymClosure R) on g) ⇒ ((SymClosure S) on f)
+  on-commutesˡ : ((SymClosure R) on g) ⇒ SymClosure (R on g)
+  on-commutesʳ : SymClosure (R on g) ⇒ ((SymClosure R) on g)
+  ```
+
 * In `Data.Vec.Relation.Binary.Pointwise.Inductive`
   ```agda
   irrelevant : ∀ {_∼_ : REL A B ℓ} {n m} → Irrelevant _∼_ → Irrelevant (Pointwise _∼_ {n} {m})
diff --git a/src/Relation/Binary/Construct/Closure/Symmetric.agda b/src/Relation/Binary/Construct/Closure/Symmetric.agda
index 369b368f20..203afc3664 100644
--- a/src/Relation/Binary/Construct/Closure/Symmetric.agda
+++ b/src/Relation/Binary/Construct/Closure/Symmetric.agda
@@ -17,7 +17,7 @@ import Relation.Binary.Construct.On as On
 private
   variable
     a ℓ ℓ₁ ℓ₂ : Level
-    A B : Set a
+    A B C : Set a
     R S : Rel A ℓ
 
 ------------------------------------------------------------------------
@@ -38,10 +38,22 @@ symmetric _ (bwd bRa) = fwd bRa
 ------------------------------------------------------------------------
 -- Operations
 
--- A generalised variant of `map` which allows the index type to change.
+-- A generalised variant of `map` where *both* index types can change.
+hmap : ∀ (g : C → A) (f : C → B) → (R on g) ⇒ (S on f) →
+       ((SymClosure R) on g) ⇒ ((SymClosure S) on f)
+hmap _ _ g*R⇒f*S (fwd aRb) = fwd (g*R⇒f*S aRb)
+hmap _ _ g*R⇒f*S (bwd bRa) = bwd (g*R⇒f*S bRa)
+
+-- Hence SymClosure commutes with `on`
+on-commutesˡ : (g : B → A) → ((SymClosure R) on g) ⇒ SymClosure (R on g)
+on-commutesˡ g = hmap g id id
+
+on-commutesʳ : (g : B → A) → SymClosure (R on g) ⇒ ((SymClosure R) on g)
+on-commutesʳ g = hmap id g id
+
+-- And: the 'usual' generalised variant of `map`
 gmap : (f : A → B) → R =[ f ]⇒ S → SymClosure R =[ f ]⇒ SymClosure S
-gmap _ g (fwd aRb) = fwd (g aRb)
-gmap _ g (bwd bRa) = bwd (g bRa)
+gmap = hmap id
 
 map : R ⇒ S → SymClosure R ⇒ SymClosure S
 map = gmap id

From 5cd81dfe4353e2e7d47e9ae531bb8bded852dd56 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 30 Mar 2026 09:02:14 +0100
Subject: [PATCH 06/15] use: new lemmas

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

diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda
index fcc2695cf1..5b6daee583 100644
--- a/src/Data/Nat/DivMod.agda
+++ b/src/Data/Nat/DivMod.agda
@@ -19,7 +19,7 @@ open import Data.Nat.Induction
 open import Data.Nat.Properties
 open import Data.Product.Base using (_,_; ∃)
 open import Data.Sum.Base using (inj₁; inj₂)
-open import Function.Base using (_$_; _∘_; _on_)
+open import Function.Base using (id; _$_; _∘_; _on_)
 open import Relation.Binary.Core using (Rel; _⇒_)
 open import Relation.Binary.Construct.Closure.Symmetric
   as SymClosure using (SymClosure; fwd; bwd)
@@ -517,16 +517,17 @@ private
   -- Example application, a result sought by Jacques Carette, taken from
   -- https://agda.zulipchat.com/#narrow/channel/264623-stdlib/topic/suc.20injective.20under.20_.25_/with/582024092
 
-  ≲%[o]-suc⁻¹ : (_≲%[ o ]_ on suc) ⇒ _≲%[ o ]_
-  ≲%[o]-suc⁻¹ (k , eq) = k , cong pred eq
-
   CarettesLemma : ∀ o .{{_ : NonZero o}} → Set _
   CarettesLemma o = (_≡[ o ]%_ on suc) ⇒ _≡[ o ]%_
 
   carettesLemma : .{{_ : NonZero o}} → CarettesLemma o
-  carettesLemma eq with ≡[o]%⇒≡%[o] eq
-  ... | fwd m≲n = ≲%[o]⇒≡[o]% (≲%[o]-suc⁻¹ m≲n)
-  ... | bwd n≲m = sym (≲%[o]⇒≡[o]% (≲%[o]-suc⁻¹ n≲m))
+  carettesLemma {o = o} = ≡%[o]⇒≡[o]% ∘ lemma-≡% ∘ ≡[o]%⇒≡%[o]
+    where
+    lemma-≲% : (_≲%[ o ]_ on suc) ⇒ _≲%[ o ]_
+    lemma-≲% (k , eq) = k , cong pred eq
+
+    lemma-≡% : (_≡%[ o ]_ on suc) ⇒ _≡%[ o ]_
+    lemma-≡% = SymClosure.hmap suc id lemma-≲%
 
   -- Alex Rice's optimised proof
   carettesLemma′ : .{{_ : NonZero o}} → CarettesLemma o

From 7306ee71529714c7f157aedfaf986dba32f96c78 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 30 Mar 2026 16:24:46 +0100
Subject: [PATCH 07/15] rename: according to review comments

---
 CHANGELOG.md                                         |  4 ++--
 src/Relation/Binary/Construct/Closure/Symmetric.agda | 10 +++++-----
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index ca02a2b1e8..cffc789bc1 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -500,8 +500,8 @@ Additions to existing modules
   ```
   hmap : ∀ (g : C → A) (f : C → B) → (R on g) ⇒ (S on f) →
          ((SymClosure R) on g) ⇒ ((SymClosure S) on f)
-  on-commutesˡ : ((SymClosure R) on g) ⇒ SymClosure (R on g)
-  on-commutesʳ : SymClosure (R on g) ⇒ ((SymClosure R) on g)
+  on⁺  : ((SymClosure R) on g) ⇒ SymClosure (R on g)
+  on⁻  : SymClosure (R on g) ⇒ ((SymClosure R) on g)
   ```
 
 * In `Data.Vec.Relation.Binary.Pointwise.Inductive`
diff --git a/src/Relation/Binary/Construct/Closure/Symmetric.agda b/src/Relation/Binary/Construct/Closure/Symmetric.agda
index 203afc3664..3ae8b2afcd 100644
--- a/src/Relation/Binary/Construct/Closure/Symmetric.agda
+++ b/src/Relation/Binary/Construct/Closure/Symmetric.agda
@@ -44,12 +44,12 @@ hmap : ∀ (g : C → A) (f : C → B) → (R on g) ⇒ (S on f) →
 hmap _ _ g*R⇒f*S (fwd aRb) = fwd (g*R⇒f*S aRb)
 hmap _ _ g*R⇒f*S (bwd bRa) = bwd (g*R⇒f*S bRa)
 
--- Hence SymClosure commutes with `on`
-on-commutesˡ : (g : B → A) → ((SymClosure R) on g) ⇒ SymClosure (R on g)
-on-commutesˡ g = hmap g id id
+-- Hence: SymClosure commutes with `on`
+on⁺ : (g : B → A) → ((SymClosure R) on g) ⇒ SymClosure (R on g)
+on⁺ g = hmap g id id
 
-on-commutesʳ : (g : B → A) → SymClosure (R on g) ⇒ ((SymClosure R) on g)
-on-commutesʳ g = hmap id g id
+on⁻ : (g : B → A) → SymClosure (R on g) ⇒ ((SymClosure R) on g)
+on⁻ g = hmap id g id
 
 -- And: the 'usual' generalised variant of `map`
 gmap : (f : A → B) → R =[ f ]⇒ S → SymClosure R =[ f ]⇒ SymClosure S

From 42b955dd8e9638eb6f56893eb4b5143c8755be4d Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 30 Mar 2026 16:38:45 +0100
Subject: [PATCH 08/15] change notation, following review comments

---
 CHANGELOG.md             | 14 +++++++-------
 src/Data/Nat/DivMod.agda | 32 ++++++++++++++++----------------
 2 files changed, 23 insertions(+), 23 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index cffc789bc1..cc4ee887a8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -321,17 +321,17 @@ Additions to existing modules
 
 * In `Data.Nat.DivMod`:
   ```agda
-  infix 4 _≲%[_]_ _≡%[_]_ : ∀ m o n → Set _
+  infix 4 _≲%[_]_ _≅%[_]_ : ∀ m o n → Set _
   m ≲%[ o ] n = ∃ λ k → n ≡ m + k * o
-  m ≡%[ o ] n = SymClosure _≲%[ o ]_ m n
+  m ≅%[ o ] n = SymClosure _≲%[ o ]_ m n
 
-  infix 4 _≡[_]%_ : ∀ m o .{{_ : NonZero o}} n → Set _
-  m ≡[ o ]% n = m % o ≡ n % o
+  infix 4 _≡%[_]_ : ∀ m o .{{_ : NonZero o}} n → Set _
+  m ≡%[ o ] n = m % o ≡ n % o
 
-  ≲%[o]⇒≡[o]% : .{{_ : NonZero o}} → _≲%[ o ]_ ⇒ _≡[ o ]%_
-  ≡%[o]⇒≡[o]% : .{{_ : NonZero o}} → _≡%[ o ]_ ⇒ _≡[ o ]%_
+  ≲%[o]⇒≡[o]% : .{{_ : NonZero o}} → _≲%[ o ]_ ⇒ _≡%[ o ]_
+  ≅%[o]⇒≡[o]% : .{{_ : NonZero o}} → _≅%[ o ]_ ⇒ _≡%[ o ]_
   ≡[o]%⇒≲%[o] : .{{_ : NonZero o}} → m % o ≡ n % o → m ≤ n → m ≲%[ o ] n
-  ≡[o]%⇒≡%[o] : .{{_ : NonZero o}} → _≡[ o ]%_ ⇒ _≡%[ o ]_
+  ≡[o]%⇒≅%[o] : .{{_ : NonZero o}} → _≡%[ o ]_ ⇒ _≅%[ o ]_
   ```
 
 * In `Data.Nat.Logarithm`
diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda
index 5b6daee583..283dcac950 100644
--- a/src/Data/Nat/DivMod.agda
+++ b/src/Data/Nat/DivMod.agda
@@ -472,28 +472,28 @@ m%n*o≡m*o%[n*o] m n o = begin-equality
 -- NB. `Relation.Binary.Construct.Closure.Symmetric`
 -- gives us the relation we're after.
 
-infix 4 _≲%[_]_ _≡%[_]_
-_≲%[_]_ _≡%[_]_ : ∀ m o n → Set _
+infix 4 _≲%[_]_ _≅%[_]_
+_≲%[_]_ _≅%[_]_ : ∀ m o n → Set _
 
 m ≲%[ o ] n = ∃ λ k → n ≡ m + k * o
-m ≡%[ o ] n = SymClosure _≲%[ o ]_ m n
+m ≅%[ o ] n = SymClosure _≲%[ o ]_ m n
 
-infix 4 _≡[_]%_
-_≡[_]%_ : ∀ m o .{{_ : NonZero o}} n → Set _
-m ≡[ o ]% n = m % o ≡ n % o
+infix 4 _≡%[_]_
+_≡%[_]_ : ∀ m o .{{_ : NonZero o}} n → Set _
+m ≡%[ o ] n = m % o ≡ n % o
 
--- Equivalence between _≡%[_]_ and _≡[_]%_
+-- Equivalence between _≅%[_]_ and _≡[_]%_
 
 module _ .{{_ : NonZero o}} where
 
-  ≲%[o]⇒≡[o]% : _≲%[ o ]_ ⇒ _≡[ o ]%_
+  ≲%[o]⇒≡[o]% : _≲%[ o ]_ ⇒ _≡%[ o ]_
   ≲%[o]⇒≡[o]% {x = m} {y = n} (k , eq) = begin-equality
     m % o           ≡⟨ [m+kn]%n≡m%n m k o ⟨
     (m + k * o) % o ≡⟨ cong (_% o) eq ⟨
     n % o ∎
 
-  ≡%[o]⇒≡[o]% : _≡%[ o ]_ ⇒ _≡[ o ]%_
-  ≡%[o]⇒≡[o]% = SymClosure.fold sym ≲%[o]⇒≡[o]%
+  ≅%[o]⇒≡[o]% : _≅%[ o ]_ ⇒ _≡%[ o ]_
+  ≅%[o]⇒≡[o]% = SymClosure.fold sym ≲%[o]⇒≡[o]%
 
   ≡[o]%⇒≲%[o] : m % o ≡ n % o → m ≤ n → m ≲%[ o ] n
   ≡[o]%⇒≲%[o] {m = m} {n = n} eq m≤n = k , (begin-equality
@@ -506,8 +506,8 @@ module _ .{{_ : NonZero o}} where
     m + k * o                   ∎)
     where k = n / o ∸ m / o
 
-  ≡[o]%⇒≡%[o] : _≡[ o ]%_ ⇒ _≡%[ o ]_
-  ≡[o]%⇒≡%[o] {x = m} {y = n} eq with ≤-total m n
+  ≡[o]%⇒≅%[o] : _≡%[ o ]_ ⇒ _≅%[ o ]_
+  ≡[o]%⇒≅%[o] {x = m} {y = n} eq with ≤-total m n
   ... | inj₁ m≤n = fwd (≡[o]%⇒≲%[o] eq m≤n)
   ... | inj₂ n≤m = bwd (≡[o]%⇒≲%[o] (sym eq) n≤m)
 
@@ -518,16 +518,16 @@ private
   -- https://agda.zulipchat.com/#narrow/channel/264623-stdlib/topic/suc.20injective.20under.20_.25_/with/582024092
 
   CarettesLemma : ∀ o .{{_ : NonZero o}} → Set _
-  CarettesLemma o = (_≡[ o ]%_ on suc) ⇒ _≡[ o ]%_
+  CarettesLemma o = (_≡%[ o ]_ on suc) ⇒ _≡%[ o ]_
 
   carettesLemma : .{{_ : NonZero o}} → CarettesLemma o
-  carettesLemma {o = o} = ≡%[o]⇒≡[o]% ∘ lemma-≡% ∘ ≡[o]%⇒≡%[o]
+  carettesLemma {o = o} = ≅%[o]⇒≡[o]% ∘ lemma-≅% ∘ ≡[o]%⇒≅%[o]
     where
     lemma-≲% : (_≲%[ o ]_ on suc) ⇒ _≲%[ o ]_
     lemma-≲% (k , eq) = k , cong pred eq
 
-    lemma-≡% : (_≡%[ o ]_ on suc) ⇒ _≡%[ o ]_
-    lemma-≡% = SymClosure.hmap suc id lemma-≲%
+    lemma-≅% : (_≅%[ o ]_ on suc) ⇒ _≅%[ o ]_
+    lemma-≅% = SymClosure.hmap suc id lemma-≲%
 
   -- Alex Rice's optimised proof
   carettesLemma′ : .{{_ : NonZero o}} → CarettesLemma o

From dae4bf392f89211879114d0e8503d72440cc55e8 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 30 Mar 2026 16:47:55 +0100
Subject: [PATCH 09/15] chnage comment text to reflect the analysis better

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

diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda
index 283dcac950..46243c044b 100644
--- a/src/Data/Nat/DivMod.agda
+++ b/src/Data/Nat/DivMod.agda
@@ -466,11 +466,11 @@ m%n*o≡m*o%[n*o] m n o = begin-equality
     p-1 * n + n ≡⟨ +-comm (p-1 * n) n ⟩
     pn          ∎
 
--- Lemmas characterising `m ≡ n (mod o)`
+-- Lemmas characterising the relation `m ≡ n (mod o)`
 
--- Definition of an asymmetric version of that notion
--- NB. `Relation.Binary.Construct.Closure.Symmetric`
--- gives us the relation we're after.
+-- Definition of an alternative, *asymmetric* version of that notion
+-- whose `Relation.Binary.Construct.Closure.Symmetric` gives us an
+-- equivalent of the above relation.
 
 infix 4 _≲%[_]_ _≅%[_]_
 _≲%[_]_ _≅%[_]_ : ∀ m o n → Set _
@@ -514,7 +514,7 @@ module _ .{{_ : NonZero o}} where
 
 private
 
-  -- Example application, a result sought by Jacques Carette, taken from
+  -- Example application, originally proposed by Jacques Carette, taken from
   -- https://agda.zulipchat.com/#narrow/channel/264623-stdlib/topic/suc.20injective.20under.20_.25_/with/582024092
 
   CarettesLemma : ∀ o .{{_ : NonZero o}} → Set _

From 02a916a2aee4c1d2c7ea7ff02f6bc46c015322f5 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 30 Mar 2026 18:03:09 +0100
Subject: [PATCH 10/15] refactor: in terms of `wlog`

---
 CHANGELOG.md             |  2 +-
 src/Data/Nat/DivMod.agda | 18 ++++++++++++++----
 2 files changed, 15 insertions(+), 5 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index cc4ee887a8..1064e85407 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -330,7 +330,7 @@ Additions to existing modules
 
   ≲%[o]⇒≡[o]% : .{{_ : NonZero o}} → _≲%[ o ]_ ⇒ _≡%[ o ]_
   ≅%[o]⇒≡[o]% : .{{_ : NonZero o}} → _≅%[ o ]_ ⇒ _≡%[ o ]_
-  ≡[o]%⇒≲%[o] : .{{_ : NonZero o}} → m % o ≡ n % o → m ≤ n → m ≲%[ o ] n
+  ≡[o]%⇒≲%[o] : .{{_ : NonZero o}} → m ≤ n → m % o ≡ n % o → m ≲%[ o ] n
   ≡[o]%⇒≅%[o] : .{{_ : NonZero o}} → _≡%[ o ]_ ⇒ _≅%[ o ]_
   ```
 
diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda
index 46243c044b..887390e8f5 100644
--- a/src/Data/Nat/DivMod.agda
+++ b/src/Data/Nat/DivMod.agda
@@ -21,6 +21,8 @@ open import Data.Product.Base using (_,_; ∃)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Function.Base using (id; _$_; _∘_; _on_)
 open import Relation.Binary.Core using (Rel; _⇒_)
+open import Relation.Binary.Consequences using (wlog)
+open import Relation.Binary.Definitions using (Symmetric)
 open import Relation.Binary.Construct.Closure.Symmetric
   as SymClosure using (SymClosure; fwd; bwd)
 open import Relation.Binary.PropositionalEquality.Core
@@ -495,8 +497,8 @@ module _ .{{_ : NonZero o}} where
   ≅%[o]⇒≡[o]% : _≅%[ o ]_ ⇒ _≡%[ o ]_
   ≅%[o]⇒≡[o]% = SymClosure.fold sym ≲%[o]⇒≡[o]%
 
-  ≡[o]%⇒≲%[o] : m % o ≡ n % o → m ≤ n → m ≲%[ o ] n
-  ≡[o]%⇒≲%[o] {m = m} {n = n} eq m≤n = k , (begin-equality
+  ≡[o]%⇒≲%[o] : m ≤ n → m % o ≡ n % o → m ≲%[ o ] n
+  ≡[o]%⇒≲%[o] {m = m} {n = n} m≤n eq = k , (begin-equality
     n                           ≡⟨ m≡m%n+[m/n]*n n o ⟩
     n % o + n / o * o           ≡⟨ cong (_+ n / o * o) eq ⟨
     m % o + n / o * o           ≡⟨ cong ((m % o +_) ∘ (_* o)) (m+[n∸m]≡n (/-monoˡ-≤ o m≤n)) ⟨
@@ -507,10 +509,18 @@ module _ .{{_ : NonZero o}} where
     where k = n / o ∸ m / o
 
   ≡[o]%⇒≅%[o] : _≡%[ o ]_ ⇒ _≅%[ o ]_
-  ≡[o]%⇒≅%[o] {x = m} {y = n} eq with ≤-total m n
+  ≡[o]%⇒≅%[o] {x = m} {y = n} =
+    wlog ≤-total symQ (λ a b a≤b → fwd ∘ ≡[o]%⇒≲%[o] a≤b) m n
+    where
+    Q : Rel ℕ _
+    Q m n = m ≡%[ o ] n → m ≅%[ o ] n
+    symQ : Symmetric Q
+    symQ mQn = SymClosure.symmetric (_≲%[ o ]_) ∘ mQn ∘ sym
+{-
+  with ≤-total m n
   ... | inj₁ m≤n = fwd (≡[o]%⇒≲%[o] eq m≤n)
   ... | inj₂ n≤m = bwd (≡[o]%⇒≲%[o] (sym eq) n≤m)
-
+-}
 
 private
 

From 4fdec645dd84e919ee0b84d913c4e27ec8a5b1a9 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 30 Mar 2026 18:33:57 +0100
Subject: [PATCH 11/15] refactor: export Jacques' lemma; leave Alex' proof
 `private`

---
 CHANGELOG.md             |  2 ++
 src/Data/Nat/DivMod.agda | 42 +++++++++++++++++++---------------------
 2 files changed, 22 insertions(+), 22 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1064e85407..b9b8fa9643 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -332,6 +332,8 @@ Additions to existing modules
   ≅%[o]⇒≡[o]% : .{{_ : NonZero o}} → _≅%[ o ]_ ⇒ _≡%[ o ]_
   ≡[o]%⇒≲%[o] : .{{_ : NonZero o}} → m ≤ n → m % o ≡ n % o → m ≲%[ o ] n
   ≡[o]%⇒≅%[o] : .{{_ : NonZero o}} → _≡%[ o ]_ ⇒ _≅%[ o ]_
+
+  ≡%-suc-injective : .{{_ : NonZero o}} → Injective _≡%[ o ]_ _≡%[ o ]_ suc
   ```
 
 * In `Data.Nat.Logarithm`
diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda
index 887390e8f5..f42ecb3a1c 100644
--- a/src/Data/Nat/DivMod.agda
+++ b/src/Data/Nat/DivMod.agda
@@ -20,6 +20,7 @@ open import Data.Nat.Properties
 open import Data.Product.Base using (_,_; ∃)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Function.Base using (id; _$_; _∘_; _on_)
+open import Function.Definitions using (Injective)
 open import Relation.Binary.Core using (Rel; _⇒_)
 open import Relation.Binary.Consequences using (wlog)
 open import Relation.Binary.Definitions using (Symmetric)
@@ -522,16 +523,11 @@ module _ .{{_ : NonZero o}} where
   ... | inj₂ n≤m = bwd (≡[o]%⇒≲%[o] (sym eq) n≤m)
 -}
 
-private
-
-  -- Example application, originally proposed by Jacques Carette, taken from
-  -- https://agda.zulipchat.com/#narrow/channel/264623-stdlib/topic/suc.20injective.20under.20_.25_/with/582024092
-
-  CarettesLemma : ∀ o .{{_ : NonZero o}} → Set _
-  CarettesLemma o = (_≡%[ o ]_ on suc) ⇒ _≡%[ o ]_
+-- Example application, originally proposed by Jacques Carette, taken from
+-- https://agda.zulipchat.com/#narrow/channel/264623-stdlib/topic/suc.20injective.20under.20_.25_/with/582024092
 
-  carettesLemma : .{{_ : NonZero o}} → CarettesLemma o
-  carettesLemma {o = o} = ≅%[o]⇒≡[o]% ∘ lemma-≅% ∘ ≡[o]%⇒≅%[o]
+  ≡%-suc-injective : Injective _≡%[ o ]_ _≡%[ o ]_ suc
+  ≡%-suc-injective = ≅%[o]⇒≡[o]% ∘ lemma-≅% ∘ ≡[o]%⇒≅%[o]
     where
     lemma-≲% : (_≲%[ o ]_ on suc) ⇒ _≲%[ o ]_
     lemma-≲% (k , eq) = k , cong pred eq
@@ -539,21 +535,23 @@ private
     lemma-≅% : (_≅%[ o ]_ on suc) ⇒ _≅%[ o ]_
     lemma-≅% = SymClosure.hmap suc id lemma-≲%
 
-  -- Alex Rice's optimised proof
-  carettesLemma′ : .{{_ : NonZero o}} → CarettesLemma o
-  carettesLemma′ {o = o@(suc d)} {x = m} {y = n} eq = begin-equality
-    m % o                   ≡⟨ lemma m ⟩
-    (suc m % o + d % o) % o ≡⟨ cong (λ a → (a + d % o) % o) eq ⟩
-    (suc n % o + d % o) % o ≡⟨ lemma n ⟨
-    n % o ∎
+private
+
+  -- Alex Rice's optimised direct proof of the above
+   ≡%[o]-suc-injective : .{{_ : NonZero o}} → Injective _≡%[ o ]_ _≡%[ o ]_ suc
+   ≡%[o]-suc-injective {o = so@(suc o)} {x = m} {y = n} eq = begin-equality
+    m % so                     ≡⟨ lemma m ⟩
+    (suc m % so + o % so) % so ≡⟨ cong (λ a → (a + o % so) % so) eq ⟩
+    (suc n % so + o % so) % so ≡⟨ lemma n ⟨
+    n % so ∎
     where
-    lemma : ∀ n → n % o ≡ (suc n % o + d % o) % o
+    lemma : ∀ n → n % so ≡ (suc n % so + o % so) % so
     lemma n = begin-equality
-      n % o                   ≡⟨ [m+n]%n≡m%n n o ⟨
-      (n + o) % o             ≡⟨⟩
-      (n + suc d) % o         ≡⟨ %-congˡ (+-suc n d) ⟩
-      (suc n + d) % o         ≡⟨ %-distribˡ-+ (suc n) d o ⟩
-      (suc n % o + d % o) % o ∎
+      n % so                     ≡⟨ [m+n]%n≡m%n n so ⟨
+      (n + so) % so              ≡⟨⟩
+      (n + suc o) % so           ≡⟨ %-congˡ (+-suc n o) ⟩
+      (suc n + o) % so           ≡⟨ %-distribˡ-+ (suc n) o so ⟩
+      (suc n % so + o % so) % so ∎
 
 
 ------------------------------------------------------------------------

From 6b7f7d8bb3af1b3a55e1209d8b8e8bf78c27bcf7 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 31 Mar 2026 10:35:19 +0100
Subject: [PATCH 12/15] refactor: comment out the `wlog` proof; tidy up the
 presentation

---
 CHANGELOG.md             |  6 +++---
 src/Data/Nat/DivMod.agda | 29 ++++++++++++++---------------
 2 files changed, 17 insertions(+), 18 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index b9b8fa9643..3b82dbbcba 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -321,13 +321,13 @@ Additions to existing modules
 
 * In `Data.Nat.DivMod`:
   ```agda
+  infix 4 _≡%[_]_ : ∀ m o .{{_ : NonZero o}} n → Set _
+  m ≡%[ o ] n = m % o ≡ n % o
+
   infix 4 _≲%[_]_ _≅%[_]_ : ∀ m o n → Set _
   m ≲%[ o ] n = ∃ λ k → n ≡ m + k * o
   m ≅%[ o ] n = SymClosure _≲%[ o ]_ m n
 
-  infix 4 _≡%[_]_ : ∀ m o .{{_ : NonZero o}} n → Set _
-  m ≡%[ o ] n = m % o ≡ n % o
-
   ≲%[o]⇒≡[o]% : .{{_ : NonZero o}} → _≲%[ o ]_ ⇒ _≡%[ o ]_
   ≅%[o]⇒≡[o]% : .{{_ : NonZero o}} → _≅%[ o ]_ ⇒ _≡%[ o ]_
   ≡[o]%⇒≲%[o] : .{{_ : NonZero o}} → m ≤ n → m % o ≡ n % o → m ≲%[ o ] n
diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda
index f42ecb3a1c..beb948d36f 100644
--- a/src/Data/Nat/DivMod.agda
+++ b/src/Data/Nat/DivMod.agda
@@ -469,11 +469,15 @@ m%n*o≡m*o%[n*o] m n o = begin-equality
     p-1 * n + n ≡⟨ +-comm (p-1 * n) n ⟩
     pn          ∎
 
+------------------------------------------------------------------------
 -- Lemmas characterising the relation `m ≡ n (mod o)`
 
--- Definition of an alternative, *asymmetric* version of that notion
--- whose `Relation.Binary.Construct.Closure.Symmetric` gives us an
--- equivalent of the above relation.
+infix 4 _≡%[_]_
+_≡%[_]_ : ∀ m o .{{_ : NonZero o}} n → Set _
+m ≡%[ o ] n = m % o ≡ n % o
+
+-- Definition of an alternative, *asymmetric* version of that relation
+-- whose `Relation.Binary.Construct.Closure.Symmetric` is equivalent.
 
 infix 4 _≲%[_]_ _≅%[_]_
 _≲%[_]_ _≅%[_]_ : ∀ m o n → Set _
@@ -481,10 +485,6 @@ _≲%[_]_ _≅%[_]_ : ∀ m o n → Set _
 m ≲%[ o ] n = ∃ λ k → n ≡ m + k * o
 m ≅%[ o ] n = SymClosure _≲%[ o ]_ m n
 
-infix 4 _≡%[_]_
-_≡%[_]_ : ∀ m o .{{_ : NonZero o}} n → Set _
-m ≡%[ o ] n = m % o ≡ n % o
-
 -- Equivalence between _≅%[_]_ and _≡[_]%_
 
 module _ .{{_ : NonZero o}} where
@@ -510,17 +510,16 @@ module _ .{{_ : NonZero o}} where
     where k = n / o ∸ m / o
 
   ≡[o]%⇒≅%[o] : _≡%[ o ]_ ⇒ _≅%[ o ]_
-  ≡[o]%⇒≅%[o] {x = m} {y = n} =
-    wlog ≤-total symQ (λ a b a≤b → fwd ∘ ≡[o]%⇒≲%[o] a≤b) m n
+  ≡[o]%⇒≅%[o] {x = m} {y = n} eq with ≤-total m n
+  ... | inj₁ m≤n = fwd (≡[o]%⇒≲%[o] m≤n eq)
+  ... | inj₂ n≤m = bwd (≡[o]%⇒≲%[o] n≤m (sym eq))
+{-
+    = wlog ≤-total symQ (λ a b a≤b → fwd ∘ ≡[o]%⇒≲%[o] a≤b) m n eq
     where
     Q : Rel ℕ _
     Q m n = m ≡%[ o ] n → m ≅%[ o ] n
     symQ : Symmetric Q
     symQ mQn = SymClosure.symmetric (_≲%[ o ]_) ∘ mQn ∘ sym
-{-
-  with ≤-total m n
-  ... | inj₁ m≤n = fwd (≡[o]%⇒≲%[o] eq m≤n)
-  ... | inj₂ n≤m = bwd (≡[o]%⇒≲%[o] (sym eq) n≤m)
 -}
 
 -- Example application, originally proposed by Jacques Carette, taken from
@@ -538,8 +537,8 @@ module _ .{{_ : NonZero o}} where
 private
 
   -- Alex Rice's optimised direct proof of the above
-   ≡%[o]-suc-injective : .{{_ : NonZero o}} → Injective _≡%[ o ]_ _≡%[ o ]_ suc
-   ≡%[o]-suc-injective {o = so@(suc o)} {x = m} {y = n} eq = begin-equality
+  ≡%[o]-suc-injective : .{{_ : NonZero o}} → Injective _≡%[ o ]_ _≡%[ o ]_ suc
+  ≡%[o]-suc-injective {o = so@(suc o)} {x = m} {y = n} eq = begin-equality
     m % so                     ≡⟨ lemma m ⟩
     (suc m % so + o % so) % so ≡⟨ cong (λ a → (a + o % so) % so) eq ⟩
     (suc n % so + o % so) % so ≡⟨ lemma n ⟨

From 135b3d90039415deddffb2f568788340ffbe4fb7 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 31 Mar 2026 10:42:43 +0100
Subject: [PATCH 13/15] removed `wlog` proof

---
 src/Data/Nat/DivMod.agda | 10 ----------
 1 file changed, 10 deletions(-)

diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda
index beb948d36f..4eff385e2e 100644
--- a/src/Data/Nat/DivMod.agda
+++ b/src/Data/Nat/DivMod.agda
@@ -22,8 +22,6 @@ open import Data.Sum.Base using (inj₁; inj₂)
 open import Function.Base using (id; _$_; _∘_; _on_)
 open import Function.Definitions using (Injective)
 open import Relation.Binary.Core using (Rel; _⇒_)
-open import Relation.Binary.Consequences using (wlog)
-open import Relation.Binary.Definitions using (Symmetric)
 open import Relation.Binary.Construct.Closure.Symmetric
   as SymClosure using (SymClosure; fwd; bwd)
 open import Relation.Binary.PropositionalEquality.Core
@@ -513,14 +511,6 @@ module _ .{{_ : NonZero o}} where
   ≡[o]%⇒≅%[o] {x = m} {y = n} eq with ≤-total m n
   ... | inj₁ m≤n = fwd (≡[o]%⇒≲%[o] m≤n eq)
   ... | inj₂ n≤m = bwd (≡[o]%⇒≲%[o] n≤m (sym eq))
-{-
-    = wlog ≤-total symQ (λ a b a≤b → fwd ∘ ≡[o]%⇒≲%[o] a≤b) m n eq
-    where
-    Q : Rel ℕ _
-    Q m n = m ≡%[ o ] n → m ≅%[ o ] n
-    symQ : Symmetric Q
-    symQ mQn = SymClosure.symmetric (_≲%[ o ]_) ∘ mQn ∘ sym
--}
 
 -- Example application, originally proposed by Jacques Carette, taken from
 -- https://agda.zulipchat.com/#narrow/channel/264623-stdlib/topic/suc.20injective.20under.20_.25_/with/582024092

From fd375b6a668ef010181810425a1420a8a6f15998 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 2 Apr 2026 09:59:25 +0100
Subject: [PATCH 14/15] refactor: appeal to `Sum` elimination, rather than
 `with`

---
 CHANGELOG.md             |  2 +-
 src/Data/Nat/DivMod.agda | 11 +++++------
 2 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3b82dbbcba..a0de4669d0 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -330,7 +330,7 @@ Additions to existing modules
 
   ≲%[o]⇒≡[o]% : .{{_ : NonZero o}} → _≲%[ o ]_ ⇒ _≡%[ o ]_
   ≅%[o]⇒≡[o]% : .{{_ : NonZero o}} → _≅%[ o ]_ ⇒ _≡%[ o ]_
-  ≡[o]%⇒≲%[o] : .{{_ : NonZero o}} → m ≤ n → m % o ≡ n % o → m ≲%[ o ] n
+  ≡[o]%⇒≲%[o] : .{{_ : NonZero o}} → m % o ≡ n % o → m ≤ n → m ≲%[ o ] n
   ≡[o]%⇒≅%[o] : .{{_ : NonZero o}} → _≡%[ o ]_ ⇒ _≅%[ o ]_
 
   ≡%-suc-injective : .{{_ : NonZero o}} → Injective _≡%[ o ]_ _≡%[ o ]_ suc
diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda
index 4eff385e2e..c50e5075dd 100644
--- a/src/Data/Nat/DivMod.agda
+++ b/src/Data/Nat/DivMod.agda
@@ -18,7 +18,7 @@ open import Data.Nat.Divisibility.Core
 open import Data.Nat.Induction
 open import Data.Nat.Properties
 open import Data.Product.Base using (_,_; ∃)
-open import Data.Sum.Base using (inj₁; inj₂)
+open import Data.Sum.Base as Sum using (inj₁; inj₂)
 open import Function.Base using (id; _$_; _∘_; _on_)
 open import Function.Definitions using (Injective)
 open import Relation.Binary.Core using (Rel; _⇒_)
@@ -496,8 +496,8 @@ module _ .{{_ : NonZero o}} where
   ≅%[o]⇒≡[o]% : _≅%[ o ]_ ⇒ _≡%[ o ]_
   ≅%[o]⇒≡[o]% = SymClosure.fold sym ≲%[o]⇒≡[o]%
 
-  ≡[o]%⇒≲%[o] : m ≤ n → m % o ≡ n % o → m ≲%[ o ] n
-  ≡[o]%⇒≲%[o] {m = m} {n = n} m≤n eq = k , (begin-equality
+  ≡[o]%⇒≲%[o] : m % o ≡ n % o → m ≤ n → m ≲%[ o ] n
+  ≡[o]%⇒≲%[o] {m = m} {n = n} eq m≤n = k , (begin-equality
     n                           ≡⟨ m≡m%n+[m/n]*n n o ⟩
     n % o + n / o * o           ≡⟨ cong (_+ n / o * o) eq ⟨
     m % o + n / o * o           ≡⟨ cong ((m % o +_) ∘ (_* o)) (m+[n∸m]≡n (/-monoˡ-≤ o m≤n)) ⟨
@@ -508,9 +508,8 @@ module _ .{{_ : NonZero o}} where
     where k = n / o ∸ m / o
 
   ≡[o]%⇒≅%[o] : _≡%[ o ]_ ⇒ _≅%[ o ]_
-  ≡[o]%⇒≅%[o] {x = m} {y = n} eq with ≤-total m n
-  ... | inj₁ m≤n = fwd (≡[o]%⇒≲%[o] m≤n eq)
-  ... | inj₂ n≤m = bwd (≡[o]%⇒≲%[o] n≤m (sym eq))
+  ≡[o]%⇒≅%[o] {x = m} {y = n} eq =
+    Sum.[ fwd ∘ ≡[o]%⇒≲%[o] eq , bwd ∘ ≡[o]%⇒≲%[o] (sym eq) ]′ (≤-total m n)
 
 -- Example application, originally proposed by Jacques Carette, taken from
 -- https://agda.zulipchat.com/#narrow/channel/264623-stdlib/topic/suc.20injective.20under.20_.25_/with/582024092

From 49d6c58b4a217a04d189d66859f96eacd98f40ff Mon Sep 17 00:00:00 2001
From: Matthew Daggitt <matthewdaggitt@gmail.com>
Date: Wed, 8 Apr 2026 21:18:00 +0800
Subject: [PATCH 15/15] Remove Zulip reference

---
 src/Data/Nat/DivMod.agda | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda
index c50e5075dd..ec7c5045dc 100644
--- a/src/Data/Nat/DivMod.agda
+++ b/src/Data/Nat/DivMod.agda
@@ -511,9 +511,6 @@ module _ .{{_ : NonZero o}} where
   ≡[o]%⇒≅%[o] {x = m} {y = n} eq =
     Sum.[ fwd ∘ ≡[o]%⇒≲%[o] eq , bwd ∘ ≡[o]%⇒≲%[o] (sym eq) ]′ (≤-total m n)
 
--- Example application, originally proposed by Jacques Carette, taken from
--- https://agda.zulipchat.com/#narrow/channel/264623-stdlib/topic/suc.20injective.20under.20_.25_/with/582024092
-
   ≡%-suc-injective : Injective _≡%[ o ]_ _≡%[ o ]_ suc
   ≡%-suc-injective = ≅%[o]⇒≡[o]% ∘ lemma-≅% ∘ ≡[o]%⇒≅%[o]
     where