Reconciling Data.Nat.Divisibility.Core._∣_ and Algebra.Definitions.RawMagma._∣_

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

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
@@ -45,8 +43,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 +109,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.

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,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 p refl) = 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 ⟩
@@ -171,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 d-1)} (divides p refl) = 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 ∎
@@ -191,7 +191,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 +203,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 +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 p refl) = +-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 p refl) = +-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 ⟩
@@ -284,7 +286,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 +356,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                               ∎

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,26 +60,28 @@ 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))
 
 ∣-refl : Reflexive _∣_
 ∣-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,20 @@ 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@.(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 ⟩
@@ -225,27 +224,30 @@ 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@.(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 p refl) = 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)
 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 +256,14 @@ 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 {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         ∎
@@ -270,24 +273,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 !_

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

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