From 618a6a940acb6b5a3a3e72c6e20e389e3a0e7160 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Tue, 26 Dec 2023 11:04:34 +0000
Subject: [PATCH 1/2] fixes issue #2237

---
 CHANGELOG.md                   |  4 ++--
 src/Data/Nat/Divisibility.agda | 18 +++++++++---------
 src/Data/Nat/Primality.agda    |  2 +-
 3 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index bf2d01d6a3..22e0b1bd30 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -58,8 +58,8 @@ Additions to existing modules
   ```agda
   quotient≢0       : m ∣ n → .{{NonZero n}} → NonZero quotient
 
-  m|n⇒n≡quotient*m : m ∣ n → n ≡ quotient * m
-  m|n⇒n≡m*quotient : m ∣ n → n ≡ m * quotient
+  m∣n⇒n≡quotient*m : m ∣ n → n ≡ quotient * m
+  m∣n⇒n≡m*quotient : m ∣ n → n ≡ m * quotient
   quotient-∣       : m ∣ n → quotient ∣ n
   quotient>1       : m ∣ n → m < n → 1 < quotient
   quotient-<       : m ∣ n → .{{NonTrivial m}} → .{{NonZero n}} → quotient < n
diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda
index abac2915a7..7b6ca61001 100644
--- a/src/Data/Nat/Divisibility.agda
+++ b/src/Data/Nat/Divisibility.agda
@@ -42,20 +42,20 @@ open import Data.Nat.Divisibility.Core public hiding (*-pres-∣)
 quotient≢0 : (m∣n : m ∣ n) → .{{NonZero n}} → NonZero (quotient m∣n)
 quotient≢0 m∣n rewrite _∣_.equality m∣n = m*n≢0⇒m≢0 (quotient m∣n)
 
-m|n⇒n≡quotient*m : (m∣n : m ∣ n) → n ≡ (quotient m∣n) * m
-m|n⇒n≡quotient*m m∣n = _∣_.equality m∣n
+m∣n⇒n≡quotient*m : (m∣n : m ∣ n) → n ≡ (quotient m∣n) * m
+m∣n⇒n≡quotient*m m∣n = _∣_.equality m∣n
 
-m|n⇒n≡m*quotient : (m∣n : m ∣ n) → n ≡ m * (quotient m∣n)
-m|n⇒n≡m*quotient {m = m} m∣n rewrite _∣_.equality m∣n = *-comm (quotient m∣n) m
+m∣n⇒n≡m*quotient : (m∣n : m ∣ n) → n ≡ m * (quotient m∣n)
+m∣n⇒n≡m*quotient {m = m} m∣n rewrite _∣_.equality m∣n = *-comm (quotient m∣n) m
 
 quotient-∣ : (m∣n : m ∣ n) → (quotient m∣n) ∣ n
-quotient-∣ {m = m} m∣n = divides m (m|n⇒n≡m*quotient m∣n)
+quotient-∣ {m = m} m∣n = divides m (m∣n⇒n≡m*quotient m∣n)
 
 quotient>1 : (m∣n : m ∣ n) → m < n → 1 < quotient m∣n
 quotient>1 {m} {n} m∣n m<n = *-cancelˡ-< m 1 (quotient m∣n) $ begin-strict
     m * 1        ≡⟨ *-identityʳ m ⟩
     m            <⟨ m<n ⟩
-    n            ≡⟨ m|n⇒n≡m*quotient m∣n ⟩
+    n            ≡⟨ m∣n⇒n≡m*quotient m∣n ⟩
     m * quotient m∣n ∎
   where open ≤-Reasoning
 
@@ -113,8 +113,8 @@ m%n≡0⇔n∣m m n = mk⇔ (m%n≡0⇒n∣m m n) (n∣m⇒m%n≡0 m n)
   divides (q * p) (sym (*-assoc q p _))
 
 ∣-antisym : Antisymmetric _≡_ _∣_
-∣-antisym {m}     {zero}   _  q∣p = m|n⇒n≡m*quotient q∣p
-∣-antisym {zero}  {n}     p∣q  _  = sym (m|n⇒n≡m*quotient p∣q)
+∣-antisym {m}     {zero}   _  q∣p = m∣n⇒n≡m*quotient q∣p
+∣-antisym {zero}  {n}     p∣q  _  = sym (m∣n⇒n≡m*quotient p∣q)
 ∣-antisym {suc m} {suc n} p∣q q∣p = ≤-antisym (∣⇒≤ p∣q) (∣⇒≤ q∣p)
 
 infix 4 _∣?_
@@ -233,7 +233,7 @@ m*n∣⇒n∣ m n rewrite *-comm m n = m*n∣⇒m∣ n m
 
 *-cancelˡ-∣ : ∀ o .{{_ : NonZero o}} → o * m ∣ o * n → m ∣ n
 *-cancelˡ-∣ {m} {n} o o*m∣o*n = divides q $ *-cancelˡ-≡ n (q * m) o $ begin-equality
-  o * n       ≡⟨ m|n⇒n≡m*quotient o*m∣o*n ⟩
+  o * n       ≡⟨ m∣n⇒n≡m*quotient o*m∣o*n ⟩
   o * m * q   ≡⟨ *-assoc o m q ⟩
   o * (m * q) ≡⟨ cong (o *_) (*-comm q m) ⟨
   o * (q * m) ∎
diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda
index 620f0c87b0..683c7d8a87 100644
--- a/src/Data/Nat/Primality.agda
+++ b/src/Data/Nat/Primality.agda
@@ -317,7 +317,7 @@ prime⇒¬composite (prime p) = p
   where 2≡1⊎2≡0 = irr[0] {2} (divides-refl 0)
 
 irreducible[1] : Irreducible 1
-irreducible[1] m|1 = inj₁ (∣1⇒≡1 m|1)
+irreducible[1] m∣1 = inj₁ (∣1⇒≡1 m∣1)
 
 irreducible[2] : Irreducible 2
 irreducible[2] {zero}  0∣2 with () ← 0∣⇒≡0 0∣2

From a4fbbc68c747efa253190eb10925cdd139a746bb Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 28 Dec 2023 12:49:39 +0000
Subject: [PATCH 2/2] leftover from #2182: subtle naming 'bug'/anomaly

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

diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda
index 7b6ca61001..f980291cc4 100644
--- a/src/Data/Nat/Divisibility.agda
+++ b/src/Data/Nat/Divisibility.agda
@@ -349,12 +349,12 @@ hasNonTrivialDivisor-≢ d≢n d∣n
 
 hasNonTrivialDivisor-∣ : m HasNonTrivialDivisorLessThan n → m ∣ o →
                          o HasNonTrivialDivisorLessThan n
-hasNonTrivialDivisor-∣ (hasNonTrivialDivisor d<n d∣m) n∣o
-  = hasNonTrivialDivisor d<n (∣-trans d∣m n∣o)
+hasNonTrivialDivisor-∣ (hasNonTrivialDivisor d<n d∣m) m∣o
+  = hasNonTrivialDivisor d<n (∣-trans d∣m m∣o)
 
 -- Monotonicity wrt ≤
 
 hasNonTrivialDivisor-≤ : m HasNonTrivialDivisorLessThan n → n ≤ o →
                          m HasNonTrivialDivisorLessThan o
-hasNonTrivialDivisor-≤ (hasNonTrivialDivisor d<n d∣m) m≤o
-  = hasNonTrivialDivisor (<-≤-trans d<n m≤o) d∣m
+hasNonTrivialDivisor-≤ (hasNonTrivialDivisor d<n d∣m) n≤o
+  = hasNonTrivialDivisor (<-≤-trans d<n n≤o) d∣m