From a7fd27125b8d44761f503ef4c95f9d71c1664060 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 2 Jul 2023 12:20:32 +0100
Subject: [PATCH 1/7] added new pattern synonym

---
 CHANGELOG.md                        |  7 +++-
 src/Data/Nat/DivMod.agda            | 18 ++++-----
 src/Data/Nat/Divisibility.agda      | 58 ++++++++++++++---------------
 src/Data/Nat/Divisibility/Core.agda |  3 ++
 4 files changed, 46 insertions(+), 40 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 5891740538..3954dd8fc7 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -901,7 +901,7 @@ Major improvements
   for them still live in `Data.Nat.DivMod` (which also publicly re-exports them
   to provide backwards compatability).
 
-* Beneficieries of this change include `Data.Rational.Unnormalised.Base` whose
+* Beneficiaries of this change include `Data.Rational.Unnormalised.Base` whose
   dependencies are now significantly smaller.
 
 ### Moved raw bundles from Data.X.Properties to Data.X.Base
@@ -2200,6 +2200,11 @@ Other minor changes
   suc-injective : Injective _≡_ _≡_ suc
   ```
 
+* Added a new pattern synonym to `Data.Nat.Divisibility.Core`:
+  ```agda
+  pattern divides-refl q = divides q refl
+  ```
+
 * Added new definitions and proofs to `Data.Nat.Primality`:
   ```agda
   Composite        : ℕ → Set
diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda
index b4c225d6a4..6a1b4edff8 100644
--- a/src/Data/Nat/DivMod.agda
+++ b/src/Data/Nat/DivMod.agda
@@ -22,8 +22,6 @@ 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
-
 open ≤-Reasoning
 
 ------------------------------------------------------------------------
@@ -91,7 +89,7 @@ m*n≤o⇒[o∸m*n]%n≡o%n m {n} {o} m*n≤o = begin-equality
 
 m∣n⇒o%n%m≡o%m : ∀ m n o .⦃ _ : NonZero m ⦄ .⦃ _ : NonZero n ⦄ → m ∣ n →
                 o % n % m ≡ o % m
-m∣n⇒o%n%m≡o%m m n o (divides p refl) = begin-equality
+m∣n⇒o%n%m≡o%m m n o (divides-refl p) = begin-equality
   o % pm % m               ≡⟨ %-congˡ (m%n≡m∸m/n*n o pm) ⟩
   (o ∸ o / pm * pm) % m    ≡˘⟨ cong (λ # → (o ∸ #) % m) (*-assoc (o / pm) p m) ⟩
   (o ∸ o / pm * p * m) % m ≡⟨ m*n≤o⇒[o∸m*n]%n≡o%n (o / pm * p) lem ⟩
@@ -171,7 +169,7 @@ m<[1+n%d]⇒m≤[n%d] {m} n (suc d-1) = k<1+a[modₕ]n⇒k≤a[modₕ]n 0 m n d-
     m′ * n′ + (m′ * j + (n′ + j * d) * k) * d         ∎
 
 %-remove-+ˡ : ∀ {m} n {d} .{{_ : NonZero d}} → d ∣ m → (m + n) % d ≡ n % d
-%-remove-+ˡ {m} n {d@(suc d-1)} (divides p refl) = begin-equality
+%-remove-+ˡ {m} n {d@(suc _)} (divides-refl p) = begin-equality
   (p * d + n) % d ≡⟨ cong (_% d) (+-comm (p * d) n) ⟩
   (n + p * d) % d ≡⟨ [m+kn]%n≡m%n n p d ⟩
   n           % d ∎
@@ -191,7 +189,7 @@ m<[1+n%d]⇒m≤[n%d] {m} n (suc d-1) = k<1+a[modₕ]n⇒k≤a[modₕ]n 0 m n d-
 /-congʳ refl = refl
 
 0/n≡0 : ∀ n .{{_ : NonZero n}} → 0 / n ≡ 0
-0/n≡0 (suc n-1) = refl
+0/n≡0 (suc _) = refl
 
 n/1≡n : ∀ n → n / 1 ≡ n
 n/1≡n n = a[divₕ]1≡a 0 n
@@ -203,7 +201,7 @@ m*n/n≡m : ∀ m n .{{_ : NonZero n}} → m * n / n ≡ m
 m*n/n≡m m (suc n-1) = a*n[divₕ]n≡a 0 m n-1
 
 m/n*n≡m : ∀ {m n} .{{_ : NonZero n}} → n ∣ m → m / n * n ≡ m
-m/n*n≡m {_} {n@(suc n-1)} (divides q refl) = cong (_* n) (m*n/n≡m q n)
+m/n*n≡m {_} {n@(suc _)} (divides-refl q) = cong (_* n) (m*n/n≡m q n)
 
 m*[n/m]≡n : ∀ {m n} .{{_ : NonZero m}} → m ∣ n → m * (n / m) ≡ n
 m*[n/m]≡n {m} m∣n = trans (*-comm m (_ / m)) (m/n*n≡m m∣n)
@@ -261,14 +259,14 @@ m≥n⇒m/n>0 {m@(suc _)} {n@(suc _)} m≥n = begin
 
 +-distrib-/-∣ˡ : ∀ {m} n {d} .{{_ : NonZero d}} →
                  d ∣ m → (m + n) / d ≡ m / d + n / d
-+-distrib-/-∣ˡ {m} n {d} (divides p refl) = +-distrib-/ m n (begin-strict
++-distrib-/-∣ˡ {m} n {d} (divides-refl p) = +-distrib-/ m n (begin-strict
   p * d % d + n % d ≡⟨ cong (_+ n % d) (m*n%n≡0 p d) ⟩
   n % d             <⟨ m%n<n n d ⟩
   d                 ∎)
 
 +-distrib-/-∣ʳ : ∀ m {n} {d} .{{_ : NonZero d}} →
                  d ∣ n → (m + n) / d ≡ m / d + n / d
-+-distrib-/-∣ʳ m {n} {d} (divides p refl) = +-distrib-/ m n (begin-strict
++-distrib-/-∣ʳ m {n} {d} (divides-refl p) = +-distrib-/ m n (begin-strict
   m % d + p * d % d ≡⟨ cong (m % d +_) (m*n%n≡0 p d) ⟩
   m % d + 0         ≡⟨ +-identityʳ _ ⟩
   m % d             <⟨ m%n<n m d ⟩
@@ -284,7 +282,7 @@ m/n≡1+[m∸n]/n {m@(suc m-1)} {n@(suc n-1)} m≥n = begin-equality
 
 m*n/m*o≡n/o : ∀ m n o .{{_ : NonZero o}} .{{_ : NonZero (m * o)}} →
               (m * n) / (m * o) ≡ n / o
-m*n/m*o≡n/o m@(suc m-1) n o = helper (<-wellFounded n)
+m*n/m*o≡n/o m@(suc _) n o = helper (<-wellFounded n)
   where
   helper : ∀ {n} → Acc _<_ n → (m * n) / (m * o) ≡ n / o
   helper {n} (acc rec) with n <? o
@@ -354,7 +352,7 @@ m/n/o≡m/[n*o] m n o = begin-equality
   m / n / o                             ≡⟨ /-congˡ {o = o} (/-congˡ (m≡m%n+[m/n]*n m n*o)) ⟩
   (m % n*o + m / n*o * n*o) / n / o     ≡⟨ /-congˡ (+-distrib-/-∣ʳ (m % n*o) lem₁) ⟩
   (m % n*o / n + m / n*o * n*o / n) / o ≡⟨ cong (λ # → (m % n*o / n + #) / o) lem₂ ⟩
-  (m % n*o / n + m / n*o * o) / o       ≡⟨ +-distrib-/-∣ʳ (m % n*o / n) (divides (m / n*o) refl) ⟩
+  (m % n*o / n + m / n*o * o) / o       ≡⟨ +-distrib-/-∣ʳ (m % n*o / n) (divides-refl (m / n*o)) ⟩
   m % n*o / n / o + m / n*o * o / o     ≡⟨ cong (m % n*o / n / o +_) (m*n/n≡m (m / n*o) o) ⟩
   m % n*o / n / o + m / n*o             ≡⟨ cong (_+ m / n*o) (m<n⇒m/n≡0 (m<n*o⇒m/o<n {n = o} lem₃)) ⟩
   m / n*o                               ∎
diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda
index c202d740ba..85df981039 100644
--- a/src/Data/Nat/Divisibility.agda
+++ b/src/Data/Nat/Divisibility.agda
@@ -39,11 +39,7 @@ m%n≡0⇒n∣m m n eq = divides (m / n) (begin-equality
   where open ≤-Reasoning
 
 n∣m⇒m%n≡0 : ∀ m n .{{_ : NonZero n}} → n ∣ m → m % n ≡ 0
-n∣m⇒m%n≡0 m n (divides v eq) = begin-equality
-  m       % n  ≡⟨ cong (_% n) eq ⟩
-  (v * n) % n  ≡⟨ m*n%n≡0 v n ⟩
-  0            ∎
-  where open ≤-Reasoning
+n∣m⇒m%n≡0 .(q * n) n (divides-refl q) = m*n%n≡0 q n
 
 m%n≡0⇔n∣m : ∀ m n .{{_ : NonZero n}} → m % n ≡ 0 ⇔ n ∣ m
 m%n≡0⇔n∣m m n = mk⇔ (m%n≡0⇒n∣m m n) (n∣m⇒m%n≡0 m n)
@@ -64,6 +60,8 @@ m%n≡0⇔n∣m m n = mk⇔ (m%n≡0⇒n∣m m n) (n∣m⇒m%n≡0 m n)
 ------------------------------------------------------------------------
 -- _∣_ is a partial order
 
+-- these could/should inherit from Algebra.Properties.Monoid.Divisibility
+
 ∣-reflexive : _≡_ ⇒ _∣_
 ∣-reflexive {n} refl = divides 1 (sym (*-identityˡ n))
 
@@ -71,19 +69,19 @@ m%n≡0⇔n∣m m n = mk⇔ (m%n≡0⇒n∣m m n) (n∣m⇒m%n≡0 m n)
 ∣-refl = ∣-reflexive refl
 
 ∣-trans : Transitive _∣_
-∣-trans (divides p refl) (divides q refl) =
+∣-trans (divides-refl p) (divides-refl q) =
   divides (q * p) (sym (*-assoc q p _))
 
 ∣-antisym : Antisymmetric _≡_ _∣_
-∣-antisym {m}     {zero}  _ (divides q refl) = *-zeroʳ q
+∣-antisym {m}     {zero}  _ (divides-refl q) = *-zeroʳ q
 ∣-antisym {zero}  {n}     (divides p eq) _   = sym (trans eq (*-comm p 0))
 ∣-antisym {suc m} {suc n} p∣q           q∣p  = ≤-antisym (∣⇒≤ p∣q) (∣⇒≤ q∣p)
 
 infix 4 _∣?_
 
 _∣?_ : Decidable _∣_
-zero  ∣? zero   = yes (divides 0 refl)
-zero  ∣? suc m  = no ((λ()) ∘′ ∣-antisym (divides 0 refl))
+zero  ∣? zero   = yes (divides-refl 0)
+zero  ∣? suc m  = no ((λ()) ∘′ ∣-antisym (divides-refl 0))
 suc n ∣? m      = Dec.map (m%n≡0⇔n∣m m (suc n)) (m % suc n ≟ 0)
 
 ∣-isPreorder : IsPreorder _≡_ _∣_
@@ -132,7 +130,7 @@ infix 10 1∣_ _∣0
 1∣ n = divides n (sym (*-identityʳ n))
 
 _∣0 : ∀ n → n ∣ 0
-n ∣0 = divides 0 refl
+n ∣0 = divides-refl 0
 
 0∣⇒≡0 : ∀ {n} → 0 ∣ n → n ≡ 0
 0∣⇒≡0 {n} 0∣n = ∣-antisym (n ∣0) 0∣n
@@ -147,7 +145,7 @@ n∣n {n} = ∣-refl
 -- Properties of _∣_ and _+_
 
 ∣m∣n⇒∣m+n : ∀ {i m n} → i ∣ m → i ∣ n → i ∣ m + n
-∣m∣n⇒∣m+n (divides p refl) (divides q refl) =
+∣m∣n⇒∣m+n (divides-refl p) (divides-refl q) =
   divides (p + q) (sym (*-distribʳ-+ _ p q))
 
 ∣m+n∣m⇒∣n : ∀ {i m n} → i ∣ m + n → i ∣ m → i ∣ n
@@ -173,19 +171,19 @@ n∣m*n*o : ∀ m {n} o → n ∣ m * n * o
 n∣m*n*o m o = ∣-trans (n∣m*n m) (m∣m*n o)
 
 ∣m⇒∣m*n : ∀ {i m} n → i ∣ m → i ∣ m * n
-∣m⇒∣m*n {i} {m} n (divides q refl) = ∣-trans (n∣m*n q) (m∣m*n n)
+∣m⇒∣m*n {i} {m} n (divides-refl q) = ∣-trans (n∣m*n q) (m∣m*n n)
 
 ∣n⇒∣m*n : ∀ {i} m {n} → i ∣ n → i ∣ m * n
 ∣n⇒∣m*n m {n} rewrite *-comm m n = ∣m⇒∣m*n m
 
 m*n∣⇒m∣ : ∀ {i} m n → m * n ∣ i → m ∣ i
-m*n∣⇒m∣ m n (divides q refl) = ∣n⇒∣m*n q (m∣m*n n)
+m*n∣⇒m∣ m n (divides-refl q) = ∣n⇒∣m*n q (m∣m*n n)
 
 m*n∣⇒n∣ : ∀ {i} m n → m * n ∣ i → n ∣ i
 m*n∣⇒n∣ m n rewrite *-comm m n = m*n∣⇒m∣ n m
 
 *-monoʳ-∣ : ∀ {i j} k → i ∣ j → k * i ∣ k * j
-*-monoʳ-∣ {i} {j} k (divides q refl) = divides q $ begin-equality
+*-monoʳ-∣ {i} {j} k (divides-refl q) = divides q $ begin-equality
   k * (q * i)  ≡⟨ sym (*-assoc k q i) ⟩
   (k * q) * i  ≡⟨ cong (_* i) (*-comm k q) ⟩
   (q * k) * i  ≡⟨ *-assoc q k i ⟩
@@ -225,14 +223,14 @@ m*n∣⇒n∣ m n rewrite *-comm m n = m*n∣⇒m∣ n m
 -- Properties of _∣_ and _/_
 
 m/n∣m : ∀ {m n} .{{_ : NonZero n}} → n ∣ m → m / n ∣ m
-m/n∣m {m} {n} (divides p refl) = begin
+m/n∣m {m} {n} (divides-refl p) = begin
   p * n / n ≡⟨ m*n/n≡m p n ⟩
   p         ∣⟨ m∣m*n n ⟩
   p * n     ∎
   where open ∣-Reasoning
 
 m*n∣o⇒m∣o/n : ∀ m n {o} .{{_ : NonZero n}} → m * n ∣ o → m ∣ o / n
-m*n∣o⇒m∣o/n m n {_} (divides p refl) = begin
+m*n∣o⇒m∣o/n m n {_} (divides-refl p) = begin
   m               ∣⟨ n∣m*n p ⟩
   p * m           ≡⟨ sym (*-identityʳ (p * m)) ⟩
   p * m * 1       ≡⟨ sym (cong (p * m *_) (n/n≡1 n)) ⟩
@@ -245,7 +243,7 @@ m*n∣o⇒n∣o/m : ∀ m n {o} .{{_ : NonZero m}} → m * n ∣ o → n ∣ (o
 m*n∣o⇒n∣o/m m n rewrite *-comm m n = m*n∣o⇒m∣o/n n m
 
 m∣n/o⇒m*o∣n : ∀ {m n o} .{{_ : NonZero o}} → o ∣ n → m ∣ n / o → m * o ∣ n
-m∣n/o⇒m*o∣n {m} {n} {o} (divides p refl) m∣p*o/o = begin
+m∣n/o⇒m*o∣n {m} {n} {o} (divides-refl p) m∣p*o/o = begin
   m * o ∣⟨ *-monoˡ-∣ o (subst (m ∣_) (m*n/n≡m p o) m∣p*o/o) ⟩
   p * o ∎
   where open ∣-Reasoning
@@ -254,13 +252,13 @@ m∣n/o⇒o*m∣n : ∀ {m n o} .{{_ : NonZero o}} → o ∣ n → m ∣ n / o 
 m∣n/o⇒o*m∣n {m} {_} {o} rewrite *-comm o m = m∣n/o⇒m*o∣n
 
 m/n∣o⇒m∣o*n : ∀ {m n o} .{{_ : NonZero n}} → n ∣ m → m / n ∣ o → m ∣ o * n
-m/n∣o⇒m∣o*n {_} {n} {o} (divides p refl) p*n/n∣o = begin
+m/n∣o⇒m∣o*n {_} {n} {o} (divides-refl p) p*n/n∣o = begin
   p * n ∣⟨ *-monoˡ-∣ n (subst (_∣ o) (m*n/n≡m p n) p*n/n∣o) ⟩
   o * n ∎
   where open ∣-Reasoning
 
 m∣n*o⇒m/n∣o : ∀ {m n o} .{{_ : NonZero n}} → n ∣ m → m ∣ o * n → m / n ∣ o
-m∣n*o⇒m/n∣o {_} {n@(suc _)} {o} (divides p refl) pn∣on = begin
+m∣n*o⇒m/n∣o {_} {n@(suc _)} {o} (divides-refl p) pn∣on = begin
   p * n / n ≡⟨ m*n/n≡m p n ⟩
   p         ∣⟨ *-cancelʳ-∣ n pn∣on ⟩
   o         ∎
@@ -270,24 +268,26 @@ m∣n*o⇒m/n∣o {_} {n@(suc _)} {o} (divides p refl) pn∣on = begin
 -- Properties of _∣_ and _%_
 
 ∣n∣m%n⇒∣m : ∀ {m n d} .{{_ : NonZero n}} → d ∣ n → d ∣ m % n → d ∣ m
-∣n∣m%n⇒∣m {m} {n} {d} (divides a n≡ad) (divides b m%n≡bd) =
+∣n∣m%n⇒∣m {m} {n@.(a * d)} {d} (divides-refl a) (divides b m%n≡bd) =
   divides (b + (m / n) * a) (begin-equality
     m                         ≡⟨ m≡m%n+[m/n]*n m n ⟩
-    m % n + (m / n) * n       ≡⟨ cong₂ _+_ m%n≡bd (cong (m / n *_) n≡ad) ⟩
+    m % n + (m / n) * n       ≡⟨ cong (_+ (m / n) * n) m%n≡bd ⟩
+    b * d + (m / n) * n       ≡⟨⟩
     b * d + (m / n) * (a * d) ≡⟨ sym (cong (b * d +_) (*-assoc (m / n) a d)) ⟩
     b * d + ((m / n) * a) * d ≡⟨ sym (*-distribʳ-+ d b _) ⟩
     (b + (m / n) * a) * d     ∎)
     where open ≤-Reasoning
 
 %-presˡ-∣ : ∀ {m n d} .{{_ : NonZero n}} → d ∣ m → d ∣ n → d ∣ m % n
-%-presˡ-∣ {m} {n} {d} (divides a refl) (divides b 1+n≡bd) =
-  divides (a ∸ ad/n * b) $ begin-equality
-    a * d % n              ≡⟨  m%n≡m∸m/n*n (a * d) n ⟩
-    a * d ∸ ad/n * n       ≡⟨  cong (λ v → a * d ∸ ad/n * v) 1+n≡bd ⟩
-    a * d ∸ ad/n * (b * d) ≡˘⟨ cong (a * d ∸_) (*-assoc ad/n b d) ⟩
-    a * d ∸ (ad/n * b) * d ≡˘⟨ *-distribʳ-∸ d a (ad/n * b) ⟩
-    (a ∸ ad/n * b) * d     ∎
-  where open ≤-Reasoning; ad/n = a * d / n
+%-presˡ-∣ {m@.(a * d)} {n} {d} (divides-refl a) (divides b 1+n≡bd) =
+  divides (a ∸ m / n * b) $ begin-equality
+    m % n                   ≡⟨  m%n≡m∸m/n*n m n ⟩
+    m ∸ m / n * n           ≡⟨  cong (λ v → m ∸ m / n * v) 1+n≡bd ⟩
+    m ∸ m / n * (b * d)     ≡˘⟨ cong (m ∸_) (*-assoc (m / n) b d) ⟩
+    m  ∸ (m / n * b) * d    ≡⟨⟩
+    a * d ∸ (m / n * b) * d ≡˘⟨ *-distribʳ-∸ d a (m / n * b) ⟩
+    (a ∸ m / n * b) * d     ∎
+  where open ≤-Reasoning
 
 ------------------------------------------------------------------------
 -- Properties of _∣_ and !_
diff --git a/src/Data/Nat/Divisibility/Core.agda b/src/Data/Nat/Divisibility/Core.agda
index 635a70c111..3b06bc2c96 100644
--- a/src/Data/Nat/Divisibility/Core.agda
+++ b/src/Data/Nat/Divisibility/Core.agda
@@ -40,6 +40,9 @@ open _∣_ using (quotient) public
 _∤_ : Rel ℕ 0ℓ
 m ∤ n = ¬ (m ∣ n)
 
+-- smart constructor
+
+pattern divides-refl q = divides q refl
 
 ------------------------------------------------------------------------
 -- Basic properties

From cc9642dd77347e4dd43e9ccaf33da691e71498dd Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 2 Jul 2023 12:50:40 +0100
Subject: [PATCH 2/7] updated `GCD` to use new pattern synonym; plus systematic
 use of irrefutable `with`

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

diff --git a/src/Data/Nat/GCD.agda b/src/Data/Nat/GCD.agda
index fe90cc0282..09991244d0 100644
--- a/src/Data/Nat/GCD.agda
+++ b/src/Data/Nat/GCD.agda
@@ -56,8 +56,8 @@ gcd m n with <-cmp m n
 gcd′[m,n]∣m,n : ∀ {m n} rec n<m → gcd′ m n rec n<m ∣ m × gcd′ m n rec n<m ∣ n
 gcd′[m,n]∣m,n {m} {zero}  rec       n<m = ∣-refl , m ∣0
 gcd′[m,n]∣m,n {m} {suc n} (acc rec) n<m
-  with gcd′[m,n]∣m,n (rec _ n<m) (m%n<n m (suc n))
-... | gcd∣n , gcd∣m%n = ∣n∣m%n⇒∣m gcd∣n gcd∣m%n , gcd∣n
+  with gcd∣n , gcd∣m%n ← gcd′[m,n]∣m,n (rec _ n<m) (m%n<n m (suc n))
+  = ∣n∣m%n⇒∣m gcd∣n gcd∣m%n , gcd∣n
 
 gcd′-greatest : ∀ {m n c} rec n<m → c ∣ m → c ∣ n → c ∣ gcd′ m n rec n<m
 gcd′-greatest {m} {zero}  rec       n<m c∣m c∣n = c∣m
@@ -166,10 +166,8 @@ gcd-universality : ∀ {m n g} →
                    (∀ {d} → d ∣ m × d ∣ n → d ∣ g) →
                    (∀ {d} → d ∣ g → d ∣ m × d ∣ n) →
                    g ≡ gcd m n
-gcd-universality {m} {n} forwards backwards with backwards ∣-refl
-... | back₁ , back₂ = ∣-antisym
-  (gcd-greatest back₁ back₂)
-  (forwards (gcd[m,n]∣m m n , gcd[m,n]∣n m n))
+gcd-universality {m} {n} forwards backwards with back₁ , back₂ ← backwards ∣-refl
+  = ∣-antisym (gcd-greatest back₁ back₂) (forwards (gcd[m,n]∣m m n , gcd[m,n]∣n m n))
 
 -- This could be simplified with some nice backwards/forwards reasoning
 -- after the new function hierarchy is up and running.
@@ -180,10 +178,10 @@ gcd[cm,cn]/c≡gcd[m,n] c m n = gcd-universality forwards backwards
   forwards {d} (d∣m , d∣n) = m*n∣o⇒n∣o/m c d (gcd-greatest (*-monoʳ-∣ c d∣m) (*-monoʳ-∣ c d∣n))
 
   backwards : ∀ {d : ℕ} → d ∣ gcd (c * m) (c * n) / c → d ∣ m × d ∣ n
-  backwards {d} d∣gcd[cm,cn]/c with m∣n/o⇒o*m∣n (gcd-greatest (m∣m*n m) (m∣m*n n)) d∣gcd[cm,cn]/c
-  ... | cd∣gcd[cm,n] =
-    *-cancelˡ-∣ c (∣-trans cd∣gcd[cm,n] (gcd[m,n]∣m (c * m) _)) ,
-    *-cancelˡ-∣ c (∣-trans cd∣gcd[cm,n] (gcd[m,n]∣n (c * m) _))
+  backwards {d} d∣gcd[cm,cn]/c
+    with cd∣gcd[cm,n] ← m∣n/o⇒o*m∣n (gcd-greatest (m∣m*n m) (m∣m*n n)) d∣gcd[cm,cn]/c
+    = *-cancelˡ-∣ c (∣-trans cd∣gcd[cm,n] (gcd[m,n]∣m (c * m) _)) ,
+      *-cancelˡ-∣ c (∣-trans cd∣gcd[cm,n] (gcd[m,n]∣n (c * m) _))
 
 c*gcd[m,n]≡gcd[cm,cn] : ∀ c m n → c * gcd m n ≡ gcd (c * m) (c * n)
 c*gcd[m,n]≡gcd[cm,cn] zero      m n = P.sym gcd[0,0]≡0
@@ -256,8 +254,8 @@ module GCD where
   -- n + k.
 
   step : ∀ {n k d} → GCD n k d → GCD n (n + k) d
-  step g with GCD.commonDivisor g
-  step {n} {k} {d} g | (d₁ , d₂) = is (d₁ , ∣m∣n⇒∣m+n d₁ d₂) greatest′
+  step {n} {k} {d} g with d₁ , d₂ ← GCD.commonDivisor g
+    = is (d₁ , ∣m∣n⇒∣m+n d₁ d₂) greatest′
     where
     greatest′ : ∀ {d′} → d′ ∣ n × d′ ∣ n + k → d′ ∣ d
     greatest′ (d₁ , d₂) = GCD.greatest g (d₁ , ∣m+n∣m⇒∣n d₂ d₁)
@@ -292,7 +290,7 @@ GCD-* {c = suc _} (GCD.is (dc∣nc , dc∣mc) dc-greatest) =
 GCD-/ : ∀ {m n d c} .{{_ : NonZero c}} → c ∣ m → c ∣ n → c ∣ d →
         GCD m n d → GCD (m / c) (n / c) (d / c)
 GCD-/ {m} {n} {d} {c} {{x}}
-  (divides p P.refl) (divides q P.refl) (divides r P.refl) gcd
+  (divides-refl p) (divides-refl q) (divides-refl r) gcd
   rewrite m*n/n≡m p c {{x}} | m*n/n≡m q c {{x}} | m*n/n≡m r c {{x}} = GCD-* gcd
 
 GCD-/gcd : ∀ m n .{{_ : NonZero (gcd m n)}} → GCD (m / gcd m n) (n / gcd m n) 1
@@ -400,6 +398,4 @@ module Bézout where
   -- Bézout's identity can be recovered from the GCD.
 
   identity : ∀ {m n d} → GCD m n d → Identity d m n
-  identity {m} {n} g with lemma m n
-  ... | result d g′ b with GCD.unique g g′
-  ...   | P.refl = b
+  identity {m} {n} g with result d g′ b ← lemma m n rewrite GCD.unique g g′ = b

From acf4e1e03c1f526e951f5fd5388446e07d36ba4c Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 2 Jul 2023 12:56:35 +0100
Subject: [PATCH 3/7] updated `Coprimality` to use new pattern synonym; plus
 systematic use of irrefutable `with`

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

diff --git a/src/Data/Nat/Coprimality.agda b/src/Data/Nat/Coprimality.agda
index 6f126a80d6..8bf92babbf 100644
--- a/src/Data/Nat/Coprimality.agda
+++ b/src/Data/Nat/Coprimality.agda
@@ -45,8 +45,8 @@ coprime⇒GCD≡1 : ∀ {m n} → Coprime m n → GCD m n 1
 coprime⇒GCD≡1 {m} {n} c = GCD.is (1∣ m , 1∣ n) (∣-reflexive ∘ c)
 
 GCD≡1⇒coprime : ∀ {m n} → GCD m n 1 → Coprime m n
-GCD≡1⇒coprime g cd with GCD.greatest g cd
-... | divides q eq = m*n≡1⇒n≡1 q _ (P.sym eq)
+GCD≡1⇒coprime g cd with divides q eq ← GCD.greatest g cd
+  = m*n≡1⇒n≡1 q _ (P.sym eq)
 
 coprime⇒gcd≡1 : ∀ {m n} → Coprime m n → gcd m n ≡ 1
 coprime⇒gcd≡1 coprime = GCD.unique (gcd-GCD _ _) (coprime⇒GCD≡1 coprime)
@@ -111,9 +111,9 @@ recompute {n} {d} c = Nullary.recompute (coprime? n d) c
 
 Bézout-coprime : ∀ {i j d} .{{_ : NonZero d}} →
                  Bézout.Identity d (i * d) (j * d) → Coprime i j
-Bézout-coprime {d = suc _} (Bézout.+- x y eq) (divides q₁ refl , divides q₂ refl) =
+Bézout-coprime {d = suc _} (Bézout.+- x y eq) (divides-refl q₁ , divides-refl q₂) =
   lem₁₀ y q₂ x q₁ eq
-Bézout-coprime {d = suc _} (Bézout.-+ x y eq) (divides q₁ refl , divides q₂ refl) =
+Bézout-coprime {d = suc _} (Bézout.-+ x y eq) (divides-refl q₁ , divides-refl q₂) =
   lem₁₀ x q₁ y q₂ eq
 
 -- Coprime numbers satisfy Bézout's identity.

From 438a196f7f522213f26f5244bdc8cad4cf278164 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 6 Jul 2023 06:54:17 +0100
Subject: [PATCH 4/7] made certain dot patterns explicit

---
 src/Data/Nat/Divisibility.agda | 17 +++++++++++------
 1 file changed, 11 insertions(+), 6 deletions(-)

diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda
index 85df981039..bb93d5e9e2 100644
--- a/src/Data/Nat/Divisibility.agda
+++ b/src/Data/Nat/Divisibility.agda
@@ -183,7 +183,8 @@ m*n∣⇒n∣ : ∀ {i} m n → m * n ∣ i → n ∣ i
 m*n∣⇒n∣ m n rewrite *-comm m n = m*n∣⇒m∣ n m
 
 *-monoʳ-∣ : ∀ {i j} k → i ∣ j → k * i ∣ k * j
-*-monoʳ-∣ {i} {j} k (divides-refl q) = divides q $ begin-equality
+*-monoʳ-∣ {i} {j@.(q * i)} k (divides-refl q) = divides q $ begin-equality
+  k * j        ≡⟨⟩
   k * (q * i)  ≡⟨ sym (*-assoc k q i) ⟩
   (k * q) * i  ≡⟨ cong (_* i) (*-comm k q) ⟩
   (q * k) * i  ≡⟨ *-assoc q k i ⟩
@@ -223,20 +224,23 @@ m*n∣⇒n∣ m n rewrite *-comm m n = m*n∣⇒m∣ n m
 -- Properties of _∣_ and _/_
 
 m/n∣m : ∀ {m n} .{{_ : NonZero n}} → n ∣ m → m / n ∣ m
-m/n∣m {m} {n} (divides-refl p) = begin
+m/n∣m {m@.(p * n)} {n} (divides-refl p) = begin
+  m / n     ≡⟨⟩
   p * n / n ≡⟨ m*n/n≡m p n ⟩
   p         ∣⟨ m∣m*n n ⟩
-  p * n     ∎
+  p * n     ≡⟨⟩
+  m         ∎
   where open ∣-Reasoning
 
 m*n∣o⇒m∣o/n : ∀ m n {o} .{{_ : NonZero n}} → m * n ∣ o → m ∣ o / n
-m*n∣o⇒m∣o/n m n {_} (divides-refl p) = begin
+m*n∣o⇒m∣o/n m n {o@.(p * (m * n))} (divides-refl p) = begin
   m               ∣⟨ n∣m*n p ⟩
   p * m           ≡⟨ sym (*-identityʳ (p * m)) ⟩
   p * m * 1       ≡⟨ sym (cong (p * m *_) (n/n≡1 n)) ⟩
   p * m * (n / n) ≡⟨ sym (*-/-assoc (p * m) (n∣n {n})) ⟩
   p * m * n / n   ≡⟨ cong (_/ n) (*-assoc p m n) ⟩
-  p * (m * n) / n ∎
+  p * (m * n) / n ≡⟨⟩
+  o / n           ∎
   where open ∣-Reasoning
 
 m*n∣o⇒n∣o/m : ∀ m n {o} .{{_ : NonZero m}} → m * n ∣ o → n ∣ (o / m)
@@ -258,7 +262,8 @@ m/n∣o⇒m∣o*n {_} {n} {o} (divides-refl p) p*n/n∣o = begin
   where open ∣-Reasoning
 
 m∣n*o⇒m/n∣o : ∀ {m n o} .{{_ : NonZero n}} → n ∣ m → m ∣ o * n → m / n ∣ o
-m∣n*o⇒m/n∣o {_} {n@(suc _)} {o} (divides-refl p) pn∣on = begin
+m∣n*o⇒m/n∣o {m@.(p * n)} {n@(suc _)} {o} (divides-refl p) pn∣on = begin
+  m / n     ≡⟨⟩
   p * n / n ≡⟨ m*n/n≡m p n ⟩
   p         ∣⟨ *-cancelʳ-∣ n pn∣on ⟩
   o         ∎

From 097893d78963b53830918a5ecbaa3b8991f6a312 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 6 Jul 2023 06:56:33 +0100
Subject: [PATCH 5/7] simplified imports

---
 src/Data/Nat/Coprimality.agda | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/Data/Nat/Coprimality.agda b/src/Data/Nat/Coprimality.agda
index 8bf92babbf..f07901cff7 100644
--- a/src/Data/Nat/Coprimality.agda
+++ b/src/Data/Nat/Coprimality.agda
@@ -9,8 +9,6 @@
 module Data.Nat.Coprimality where
 
 open import Data.Empty
-open import Data.Fin.Base using (toℕ; fromℕ<)
-open import Data.Fin.Properties using (toℕ-fromℕ<)
 open import Data.Nat.Base
 open import Data.Nat.Divisibility
 open import Data.Nat.GCD

From c4aa993daea1443a3606e2e036c79cc752aaa515 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 6 Jul 2023 07:00:28 +0100
Subject: [PATCH 6/7] simplified imports

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

diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda
index e634095eea..f2a9cb0d5f 100644
--- a/src/Data/Nat/Primality.agda
+++ b/src/Data/Nat/Primality.agda
@@ -21,7 +21,7 @@ open import Relation.Nullary.Decidable as Dec
 open import Relation.Nullary.Negation using (¬_; contradiction)
 open import Relation.Unary using (Decidable)
 open import Relation.Binary.PropositionalEquality
-  using (refl; sym; cong; subst)
+  using (refl; cong)
 
 private
   variable

From 5e4a5e3010c74fb95a6f0b1f794ff067bd7b40a1 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 6 Jul 2023 07:45:59 +0100
Subject: [PATCH 7/7] more explicit dot patterns

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

diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda
index 6a1b4edff8..c879cec098 100644
--- a/src/Data/Nat/DivMod.agda
+++ b/src/Data/Nat/DivMod.agda
@@ -89,7 +89,8 @@ m*n≤o⇒[o∸m*n]%n≡o%n m {n} {o} m*n≤o = begin-equality
 
 m∣n⇒o%n%m≡o%m : ∀ m n o .⦃ _ : NonZero m ⦄ .⦃ _ : NonZero n ⦄ → m ∣ n →
                 o % n % m ≡ o % m
-m∣n⇒o%n%m≡o%m m n o (divides-refl p) = begin-equality
+m∣n⇒o%n%m≡o%m m n@.(p * m) o (divides-refl p) = begin-equality
+  o % n % m                ≡⟨⟩
   o % pm % m               ≡⟨ %-congˡ (m%n≡m∸m/n*n o pm) ⟩
   (o ∸ o / pm * pm) % m    ≡˘⟨ cong (λ # → (o ∸ #) % m) (*-assoc (o / pm) p m) ⟩
   (o ∸ o / pm * p * m) % m ≡⟨ m*n≤o⇒[o∸m*n]%n≡o%n (o / pm * p) lem ⟩
@@ -169,7 +170,8 @@ m<[1+n%d]⇒m≤[n%d] {m} n (suc d-1) = k<1+a[modₕ]n⇒k≤a[modₕ]n 0 m n d-
     m′ * n′ + (m′ * j + (n′ + j * d) * k) * d         ∎
 
 %-remove-+ˡ : ∀ {m} n {d} .{{_ : NonZero d}} → d ∣ m → (m + n) % d ≡ n % d
-%-remove-+ˡ {m} n {d@(suc _)} (divides-refl p) = begin-equality
+%-remove-+ˡ {m@.(p * d)} n {d@(suc _)} (divides-refl p) = begin-equality
+  (m + n)     % d ≡⟨⟩
   (p * d + n) % d ≡⟨ cong (_% d) (+-comm (p * d) n) ⟩
   (n + p * d) % d ≡⟨ [m+kn]%n≡m%n n p d ⟩
   n           % d ∎
@@ -259,14 +261,16 @@ m≥n⇒m/n>0 {m@(suc _)} {n@(suc _)} m≥n = begin
 
 +-distrib-/-∣ˡ : ∀ {m} n {d} .{{_ : NonZero d}} →
                  d ∣ m → (m + n) / d ≡ m / d + n / d
-+-distrib-/-∣ˡ {m} n {d} (divides-refl p) = +-distrib-/ m n (begin-strict
++-distrib-/-∣ˡ {m@.(p * d)} n {d} (divides-refl p) = +-distrib-/ m n (begin-strict
+  m % d + n % d     ≡⟨⟩
   p * d % d + n % d ≡⟨ cong (_+ n % d) (m*n%n≡0 p d) ⟩
   n % d             <⟨ m%n<n n d ⟩
   d                 ∎)
 
 +-distrib-/-∣ʳ : ∀ m {n} {d} .{{_ : NonZero d}} →
                  d ∣ n → (m + n) / d ≡ m / d + n / d
-+-distrib-/-∣ʳ m {n} {d} (divides-refl p) = +-distrib-/ m n (begin-strict
++-distrib-/-∣ʳ m {n@.(p * d)} {d} (divides-refl p) = +-distrib-/ m n (begin-strict
+  m % d + n % d     ≡⟨⟩
   m % d + p * d % d ≡⟨ cong (m % d +_) (m*n%n≡0 p d) ⟩
   m % d + 0         ≡⟨ +-identityʳ _ ⟩
   m % d             <⟨ m%n<n m d ⟩