From c649694289adc712498ea60468ebcb5ace447cb2 Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Thu, 14 Dec 2023 06:05:35 +0000
Subject: [PATCH] [fixes #1711] Refactoring `Data.Nat.Divisibility` and
 `Data.Nat.DivMod` (#2182)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* added new definitions to `_∣_`

* `CHANGELOG`

* don't declare `quotient≢0` as an `instance`

* replace use of `subst` with one of `trans`

* what's sauce for the goose...

* switch to a `rewrite`-based solution...

* tightened `import`s

* simplified dependenciess

* simplified dependencies; `CHANGELOG`

* removed `module` abstractions

* delegated proof of `quotient≢0` to `Data.Nat.Properties`

* removed redundant property

* cosmetic review changes; others to follow

* better proof of `quotient>1`

* `where` clause layout

* leaving in the flipped equality; moved everything else

* new lemmas moved from `Core`; knock-on consequences; lots of tidying up

* tidying up; `CHANGELOG`

* cosmetic tweaks

* reverted to simple version

* problems with exporting `quotient`

* added last lemma: defining equation for `_/_`

* improved `CHANGELOG`

* revert: simplified imports

* improved `CHANGELOG`

* endpoint of simplifying the proof of `*-pres-∣`

* simplified the proof of `n/m≡quotient`

* simplified the proof of `∣m+n∣m⇒∣n`

* simplified the proof of `∣m∸n∣n⇒∣m`

* simplified `import`s

* simplified a lot of proofs, esp. wrt `divides-refl` and `NonZero` reasoning

* simplified more proofs, esp. wrt `divides-refl` reasoning

* simplified `import`s

* moved `equalityᵒ` proof out of `Core`

* `CHANGELOG`

* temporary fix: further `NonZero` refactoring advised!

* regularised use of instance brackets

* further instance simplification

* further streamlining

* tidied up `CHANGELOG`

* simplified `NonZero` pattern matching

* regularised use of instance brackets

* simplified proof of `/-*-interchange`

* simplified proof of `/-*-interchange`

* ... permitting the migration of `*-pres-∣` to `Data.Nat.Divisibility`

* tweaked proof of `/-*-interchange`

* narrowed `import`s

* simplified proof; renamed new proofs

* Capitalisation

* streamlined `import`s; streamlined proof of decidability

* spurious duplication after merge

* missing symbol import

* replaced one use of `1 < m` with `{{NonTrivial m}}`

* fixed `CHANGELOG`

* removed use of identifier `k`

* refactoring: more use of `NonTrivial` instances

* knock-on consequences: simplified function

* two new lemmas

* refactoring: use of `connex` in proofs

* new lemmas about `pred`

* new lemmas about monus

* refactoring: use of the new properties, simplifying pattern analysis

* whitespace

* questionable? revision after comments on #2221

* silly argument name typo; remove parens

* tidied up imports of `Relation.Nullary`

* removed spurious `instance`

* localised appeals to `Reasoning`

* further use of `variable`s

* tidied up `record` name in comment

* cosmetic

* reconciled implicit/explicit arguments in various monus lemmas

* fixed knock-on change re monus; reverted change to `m/n<m`

* reverted change to `m/n≢0⇒n≤m`

* reverted breaking changes involving `NonZero` inference

* revised `CHANGELOG`

* restored deleted proof

* fix whitespace

* renaming: `DivMod.nonZeroDivisor`

* localised use of `≤-Reasoning`

* reverted export; removed anonymous module

* revert commit re `yes/no`

* renamed flipped equality

* tweaked comment

* added alias for `equality`
---
 CHANGELOG.md                        |  43 ++++-
 src/Data/Digit.agda                 |   7 +-
 src/Data/Fin/Properties.agda        |   3 +
 src/Data/Nat/Coprimality.agda       |  14 +-
 src/Data/Nat/DivMod.agda            | 253 ++++++++++++------------
 src/Data/Nat/Divisibility.agda      | 285 +++++++++++++++-------------
 src/Data/Nat/Divisibility/Core.agda |  38 ++--
 src/Data/Nat/Properties.agda        |  53 ++++--
 src/Data/Rational/Properties.agda   |  11 +-
 9 files changed, 407 insertions(+), 300 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2701cdde9b..bf2d01d6a3 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -21,15 +21,20 @@ Deprecated modules
 Deprecated names
 ----------------
 
+* In `Data.Nat.Divisibility.Core`:
+  ```agda
+  *-pres-∣  ↦  Data.Nat.Divisibility.*-pres-∣
+  ```
+
 New modules
 -----------
 
 Additions to existing modules
 -----------------------------
 
-* In `Data.Maybe.Relation.Binary.Pointwise`:
+* In `Data.Fin.Properties`:
   ```agda
-  pointwise⊆any : Pointwise R (just x) ⊆ Any (R x)
+  nonZeroIndex : Fin n → ℕ.NonZero n
   ```
 
 * In `Data.List.Relation.Unary.All.Properties`:
@@ -39,7 +44,39 @@ Additions to existing modules
   ```
 
 * In `Data.List.Relation.Unary.AllPairs.Properties`:
-  ```
+  ```agda
   catMaybes⁺ : AllPairs (Pointwise R) xs → AllPairs R (catMaybes xs)
   tabulate⁺-< : (i < j → R (f i) (f j)) → AllPairs R (tabulate f)
   ```
+
+* In `Data.Maybe.Relation.Binary.Pointwise`:
+  ```agda
+  pointwise⊆any : Pointwise R (just x) ⊆ Any (R x)
+  ```
+
+* In `Data.Nat.Divisibility`:
+  ```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
+  quotient-∣       : m ∣ n → quotient ∣ n
+  quotient>1       : m ∣ n → m < n → 1 < quotient
+  quotient-<       : m ∣ n → .{{NonTrivial m}} → .{{NonZero n}} → quotient < n
+  n/m≡quotient     : m ∣ n → .{{_ : NonZero m}} → n / m ≡ quotient
+
+  m/n≡0⇒m<n    : .{{_ : NonZero n}} → m / n ≡ 0 → m < n
+  m/n≢0⇒n≤m    : .{{_ : NonZero n}} → m / n ≢ 0 → n ≤ m
+
+  nonZeroDivisor : DivMod dividend divisor → NonZero divisor
+  ```
+
+* Added new proofs in `Data.Nat.Properties`:
+  ```agda
+  m≤n+o⇒m∸n≤o : ∀ m n {o} → m ≤ n + o → m ∸ n ≤ o
+  m<n+o⇒m∸n<o : ∀ m n {o} → .{{NonZero o}} → m < n + o → m ∸ n < o
+  pred-cancel-≤ : pred m ≤ pred n → (m ≡ 1 × n ≡ 0) ⊎ m ≤ n
+  pred-cancel-< : pred m < pred n → m < n
+  pred-injective : .{{NonZero m}} → .{{NonZero n}} → pred m ≡ pred n → m ≡ n
+  pred-cancel-≡ : pred m ≡ pred n → ((m ≡ 0 × n ≡ 1) ⊎ (m ≡ 1 × n ≡ 0)) ⊎ m ≡ n
+  ```
diff --git a/src/Data/Digit.agda b/src/Data/Digit.agda
index 3f11c1c3af..207b0280b7 100644
--- a/src/Data/Digit.agda
+++ b/src/Data/Digit.agda
@@ -55,11 +55,8 @@ toNatDigits base@(suc (suc _)) n = aux (<-wellFounded-fast n) []
   aux : {n : ℕ} → Acc _<_ n → List ℕ → List ℕ
   aux {zero}        _      xs =  (0 ∷ xs)
   aux {n@(suc _)} (acc wf) xs with does (0 <? n / base)
-  ... | false = (n % base) ∷ xs
-  ... | true  = aux (wf q<n) ((n % base) ∷ xs)
-    where
-    q<n : n / base < n
-    q<n = m/n<m n base (s<s z<s)
+  ... | false = (n % base) ∷ xs -- Could this more simply be n ∷ xs here?
+  ... | true  = aux (wf (m/n<m n base sz<ss)) ((n % base) ∷ xs)
 
 ------------------------------------------------------------------------
 -- Converting between `ℕ` and expansions of `Digit base`
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index cdcbeb4e85..303cf64905 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -65,6 +65,9 @@ private
 ¬Fin0 : ¬ Fin 0
 ¬Fin0 ()
 
+nonZeroIndex : Fin n → ℕ.NonZero n
+nonZeroIndex {n = suc _} _ = _
+
 ------------------------------------------------------------------------
 -- Bundles
 
diff --git a/src/Data/Nat/Coprimality.agda b/src/Data/Nat/Coprimality.agda
index f385944f50..f513e82fa4 100644
--- a/src/Data/Nat/Coprimality.agda
+++ b/src/Data/Nat/Coprimality.agda
@@ -21,7 +21,7 @@ open import Function.Base using (_∘_)
 open import Level using (0ℓ)
 open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; _≢_; refl; trans; cong; subst)
-open import Relation.Nullary as Nullary using (¬_; contradiction; yes ; no)
+open import Relation.Nullary as Nullary using (¬_; contradiction; map′)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions using (Symmetric; Decidable)
 
@@ -65,18 +65,8 @@ coprime-/gcd m n = GCD≡1⇒coprime (GCD-/gcd m n)
 sym : Symmetric Coprime
 sym c = c ∘ swap
 
-private
-  0≢1 : 0 ≢ 1
-  0≢1 ()
-
-  2+≢1 : ∀ {n} → 2+ n ≢ 1
-  2+≢1 ()
-
 coprime? : Decidable Coprime
-coprime? m n with mkGCD m n
-... | (0    , g) = no  (0≢1  ∘ GCD.unique g ∘ coprime⇒GCD≡1)
-... | (1    , g) = yes (GCD≡1⇒coprime g)
-... | (2+ _ , g) = no  (2+≢1 ∘ GCD.unique g ∘ coprime⇒GCD≡1)
+coprime? m n = map′ gcd≡1⇒coprime coprime⇒gcd≡1 (gcd m n ≟ 1)
 
 ------------------------------------------------------------------------
 -- Other basic properties
diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda
index bbb8288838..5ff23e4c72 100644
--- a/src/Data/Nat/DivMod.agda
+++ b/src/Data/Nat/DivMod.agda
@@ -11,15 +11,16 @@ module Data.Nat.DivMod where
 open import Agda.Builtin.Nat using (div-helper; mod-helper)
 
 open import Data.Fin.Base using (Fin; toℕ; fromℕ<)
-open import Data.Fin.Properties using (toℕ-fromℕ<)
-open import Data.Nat.Base as Nat
+open import Data.Fin.Properties using (nonZeroIndex; toℕ-fromℕ<)
+open import Data.Nat.Base
 open import Data.Nat.DivMod.Core
 open import Data.Nat.Divisibility.Core
 open import Data.Nat.Induction
 open import Data.Nat.Properties
-open import Function.Base using (_$_)
+open import Data.Sum.Base using (inj₁; inj₂)
+open import Function.Base using (_$_; _∘_)
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary.Decidable using (yes; no)
+open import Relation.Nullary.Negation using (contradiction)
 
 open ≤-Reasoning
 
@@ -34,7 +35,7 @@ open import Data.Nat.Base public
   using (_%_; _/_)
 
 ------------------------------------------------------------------------
--- Relationship between _%_ and _div_
+-- Relationship between _%_ and _/_
 
 m≡m%n+[m/n]*n : ∀ m n .{{_ : NonZero n}} → m ≡ m % n + (m / n) * n
 m≡m%n+[m/n]*n m (suc n) = div-mod-lemma 0 0 m n
@@ -49,10 +50,10 @@ m%n≡m∸m/n*n m n = begin-equality
 ------------------------------------------------------------------------
 -- Properties of _%_
 
-%-congˡ : .⦃ _ : NonZero o ⦄ → m ≡ n → m % o ≡ n % o
+%-congˡ : .{{_ : NonZero o}} → m ≡ n → m % o ≡ n % o
 %-congˡ refl = refl
 
-%-congʳ : .⦃ _ : NonZero m ⦄ .⦃ _ : NonZero n ⦄ → m ≡ n →
+%-congʳ : .{{_ : NonZero m}} .{{_ : NonZero n}} → m ≡ n →
           o % m ≡ o % n
 %-congʳ refl = refl
 
@@ -71,45 +72,25 @@ m%n%n≡m%n m (suc n-1) = modₕ-idem 0 m n-1
 [m+kn]%n≡m%n : ∀ m k n .{{_ : NonZero n}} → (m + k * n) % n ≡ m % n
 [m+kn]%n≡m%n m zero    n = cong (_% n) (+-identityʳ m)
 [m+kn]%n≡m%n m (suc k) n = begin-equality
-  (m + (n + k * n)) % n ≡⟨ cong (_% n) (sym (+-assoc m n (k * n))) ⟩
+  (m + (n + k * n)) % n ≡⟨ cong (_% n) (+-assoc m n (k * n)) ⟨
   (m + n + k * n)   % n ≡⟨ [m+kn]%n≡m%n (m + n) k n ⟩
   (m + n)           % n ≡⟨ [m+n]%n≡m%n m n ⟩
   m                 % n ∎
 
-m≤n⇒[n∸m]%m≡n%m : .⦃ _ : NonZero m ⦄ → m ≤ n →
+m≤n⇒[n∸m]%m≡n%m : .{{_ : NonZero m}} → m ≤ n →
                   (n ∸ m) % m ≡ n % m
 m≤n⇒[n∸m]%m≡n%m {m} {n} m≤n = begin-equality
   (n ∸ m) % m     ≡⟨ [m+n]%n≡m%n (n ∸ m) m ⟨
   (n ∸ m + m) % m ≡⟨ cong (_% m) (m∸n+n≡m m≤n) ⟩
   n % m           ∎
 
-m*n≤o⇒[o∸m*n]%n≡o%n : ∀ m {n o} .⦃ _ : NonZero n ⦄ → m * n ≤ o →
+m*n≤o⇒[o∸m*n]%n≡o%n : ∀ m {n o} .{{_ : NonZero n}} → m * n ≤ o →
                       (o ∸ m * n) % n ≡ o % n
 m*n≤o⇒[o∸m*n]%n≡o%n m {n} {o} m*n≤o = begin-equality
   (o ∸ m * n) % n         ≡⟨ [m+kn]%n≡m%n (o ∸ m * n) m n ⟨
   (o ∸ m * n + m * n) % n ≡⟨ cong (_% n) (m∸n+n≡m m*n≤o) ⟩
   o % n                   ∎
 
-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@.(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 ⟩
-  o % m                    ∎
-  where
-  pm = p * m
-
-  lem : o / pm * p * m ≤ o
-  lem = begin
-    o / pm * p * m       ≡⟨ *-assoc (o / pm) p m ⟩
-    -- Sort out dependencies in this file, then use m/n*n≤m instead.
-    o / pm * pm          ≤⟨ m≤m+n (o / pm * pm) (o % pm) ⟩
-    o / pm * pm + o % pm ≡⟨ +-comm _ (o % pm) ⟩
-    o % pm + o / pm * pm ≡⟨ m≡m%n+[m/n]*n o pm ⟨
-    o                    ∎
-
 m*n%n≡0 : ∀ m n .{{_ : NonZero n}} → (m * n) % n ≡ 0
 m*n%n≡0 m n@(suc _) = [m+kn]%n≡m%n 0 m n
 
@@ -123,10 +104,10 @@ m%n≤m : ∀ m n .{{_ : NonZero n}} → m % n ≤ m
 m%n≤m m (suc n-1) = a[modₕ]n≤a 0 m n-1
 
 m≤n⇒m%n≡m : m ≤ n → m % suc n ≡ m
-m≤n⇒m%n≡m {m = m} m≤n with less-than-or-equal {k} refl ← ≤⇒≤″ m≤n
+m≤n⇒m%n≡m {m = m} m≤n with ≤″-offset k ← ≤⇒≤″ m≤n
   = a≤n⇒a[modₕ]n≡a 0 (m + k) m k
 
-m<n⇒m%n≡m : .⦃ _ : NonZero n ⦄ → m < n → m % n ≡ m
+m<n⇒m%n≡m : .{{_ : NonZero n}} → m < n → m % n ≡ m
 m<n⇒m%n≡m {n = suc _} m<n = m≤n⇒m%n≡m (<⇒≤pred m<n)
 
 %-pred-≡0 : ∀ {m n} .{{_ : NonZero n}} → (suc m % n) ≡ 0 → (m % n) ≡ n ∸ 1
@@ -143,15 +124,15 @@ 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)                         % d ≡⟨ cong (λ v → (v + n) % d) (m≡m%n+[m/n]*n m d) ⟩
   (m % d +  m / d * d + n)        % d ≡⟨ cong (_% d) (+-assoc (m % d) _ n) ⟩
   (m % d + (m / d * d + n))       % d ≡⟨ cong (λ v → (m % d + v) % d) (+-comm _ n) ⟩
-  (m % d + (n + m / d * d))       % d ≡⟨ cong (_% d) (sym (+-assoc (m % d) n _)) ⟩
+  (m % d + (n + m / d * d))       % d ≡⟨ cong (_% d) (+-assoc (m % d) n _) ⟨
   (m % d +  n + m / d * d)        % d ≡⟨ [m+kn]%n≡m%n (m % d + n) (m / d) d ⟩
   (m % d +  n)                    % d ≡⟨ cong (λ v → (m % d + v) % d) (m≡m%n+[m/n]*n n d) ⟩
-  (m % d + (n % d + (n / d) * d)) % d ≡⟨ sym (cong (_% d) (+-assoc (m % d) (n % d) _)) ⟩
+  (m % d + (n % d + (n / d) * d)) % d ≡⟨ cong (_% d) (+-assoc (m % d) (n % d) _) ⟨
   (m % d +  n % d + (n / d) * d)  % d ≡⟨ [m+kn]%n≡m%n (m % d + n % d) (n / d) d ⟩
   (m % d +  n % d)                % d ∎
 
 %-distribˡ-* : ∀ m n d .{{_ : NonZero d}} → (m * n) % d ≡ ((m % d) * (n % d)) % d
-%-distribˡ-* m n d@(suc d-1) = begin-equality
+%-distribˡ-* m n d = begin-equality
   (m * n)                                             % d ≡⟨ cong (λ h → (h * n) % d) (m≡m%n+[m/n]*n m d) ⟩
   ((m′ + k * d) * n)                                  % d ≡⟨ cong (λ h → ((m′ + k * d) * h) % d) (m≡m%n+[m/n]*n n d) ⟩
   ((m′ + k * d) * (n′ + j * d))                       % d ≡⟨ cong (_% d) lemma ⟩
@@ -173,14 +154,14 @@ 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@.(p * d)} n {d@(suc _)} (divides-refl p) = begin-equality
+%-remove-+ˡ {m@.(p * d)} n {d} (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 ∎
 
 %-remove-+ʳ : ∀ m {n d} .{{_ : NonZero d}} → d ∣ n → (m + n) % d ≡ m % d
-%-remove-+ʳ m {n} {suc _} eq rewrite +-comm m n = %-remove-+ˡ {n} m eq
+%-remove-+ʳ m {n} rewrite +-comm m n = %-remove-+ˡ {n} m
 
 ------------------------------------------------------------------------
 -- Properties of _/_
@@ -204,16 +185,16 @@ 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 _)} (divides-refl q) = cong (_* n) (m*n/n≡m q n)
+m/n*n≡m {n = n} (divides-refl q) = cong (_* n) (m*n/n≡m q 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)
 
 m/n*n≤m : ∀ m n .{{_ : NonZero n}} → (m / n) * n ≤ m
-m/n*n≤m m n@(suc n-1) = begin
+m/n*n≤m m n = begin
   (m / n) * n          ≤⟨ m≤m+n ((m / n) * n) (m % n) ⟩
   (m / n) * n + m % n  ≡⟨ +-comm _ (m % n) ⟩
-  m % n + (m / n) * n  ≡⟨ sym (m≡m%n+[m/n]*n m n) ⟩
+  m % n + (m / n) * n  ≡⟨ m≡m%n+[m/n]*n m n ⟨
   m                    ∎
 
 m/n≤m : ∀ m n .{{_ : NonZero n}} → (m / n) ≤ m
@@ -222,11 +203,12 @@ m/n≤m m n = *-cancelʳ-≤ (m / n) m n (begin
   m           ≤⟨ m≤m*n m n ⟩
   m * n       ∎)
 
-m/n<m : ∀ m n .{{_ : NonZero m}} .{{_ : NonZero n}} → n ≥ 2 → m / n < m
-m/n<m m n n≥2 = *-cancelʳ-< _ (m / n) m (begin-strict
-  (m / n) * n ≤⟨ m/n*n≤m m n ⟩
-  m           <⟨ m<m*n m n n≥2 ⟩
-  m * n       ∎)
+m/n<m : ∀ m n .{{_ : NonZero m}} .{{_ : NonZero n}} →
+        1 < n → m / n < m
+m/n<m m n 1<n = *-cancelʳ-< _ (m / n) m $ begin-strict
+  m / n * n ≤⟨ m/n*n≤m m n ⟩
+  m         <⟨ m<m*n m n 1<n ⟩
+  m * n     ∎
 
 /-mono-≤ : .{{_ : NonZero o}} .{{_ : NonZero p}} →
            m ≤ n → o ≥ p → m / o ≤ n / p
@@ -243,8 +225,8 @@ m/n<m m n n≥2 = *-cancelʳ-< _ (m / n) m (begin-strict
               o ∣ m → o ∣ n → m / o ≡ n / o → m ≡ n
 /-cancelʳ-≡ {m} {n} {o} o∣m o∣n m/o≡n/o = begin-equality
   m           ≡⟨ m*[n/m]≡n {o} {m} o∣m ⟨
-  o * (m / o) ≡⟨  cong (o *_) m/o≡n/o ⟩
-  o * (n / o) ≡⟨  m*[n/m]≡n {o} {n} o∣n ⟩
+  o * (m / o) ≡⟨ cong (o *_) m/o≡n/o ⟩
+  o * (n / o) ≡⟨ m*[n/m]≡n {o} {n} o∣n ⟩
   n           ∎
 
 m<n⇒m/n≡0 : ∀ {m n} .{{_ : NonZero n}} → m < n → m / n ≡ 0
@@ -252,30 +234,41 @@ m<n⇒m/n≡0 {m} {suc n-1} (s≤s m≤n) = divₕ-finish n-1 m n-1 m≤n
 
 m≥n⇒m/n>0 : ∀ {m n} .{{_ : NonZero n}} → m ≥ n → m / n > 0
 m≥n⇒m/n>0 {m@(suc _)} {n@(suc _)} m≥n = begin
-  1     ≡⟨ sym (n/n≡1 m) ⟩
+  1     ≡⟨ n/n≡1 m ⟨
   m / m ≤⟨ /-monoʳ-≤ m m≥n ⟩
   m / n ∎
 
+m/n≡0⇒m<n : ∀ {m n} .{{_ : NonZero n}} → m / n ≡ 0 → m < n
+m/n≡0⇒m<n {m} {n@(suc _)} m/n≡0  with <-≤-connex m n
+... | inj₁ m<n = m<n
+... | inj₂ n≤m = contradiction m/n≡0 (≢-nonZero⁻¹ _)
+  where instance _ =  >-nonZero (m≥n⇒m/n>0 n≤m)
+
+m/n≢0⇒n≤m : ∀ {m n} .{{_ : NonZero n}} → m / n ≢ 0 → n ≤ m
+m/n≢0⇒n≤m {m} {n@(suc _)} m/n≢0 with <-≤-connex m n
+... | inj₁ m<n = contradiction (m<n⇒m/n≡0 m<n) m/n≢0
+... | inj₂ n≤m = n≤m
+
 +-distrib-/ : ∀ m n {d} .{{_ : NonZero d}} → m % d + n % d < d →
               (m + n) / d ≡ m / d + n / d
 +-distrib-/ m n {suc d-1} leq = +-distrib-divₕ 0 0 m n d-1 leq
 
 +-distrib-/-∣ˡ : ∀ {m} n {d} .{{_ : NonZero d}} →
                  d ∣ m → (m + n) / d ≡ m / d + n / d
-+-distrib-/-∣ˡ {m@.(p * d)} 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                 ∎)
+  d                 ∎
 
 +-distrib-/-∣ʳ : ∀ m {n} {d} .{{_ : NonZero d}} →
                  d ∣ n → (m + n) / d ≡ m / d + n / d
-+-distrib-/-∣ʳ m {n@.(p * d)} {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 ⟩
-  d                 ∎)
+  d                 ∎
 
 m/n≡1+[m∸n]/n : ∀ {m n} .{{_ : NonZero n}} → m ≥ n → m / n ≡ 1 + ((m ∸ n) / n)
 m/n≡1+[m∸n]/n {m@(suc m-1)} {n@(suc n-1)} m≥n = begin-equality
@@ -285,64 +278,77 @@ m/n≡1+[m∸n]/n {m@(suc m-1)} {n@(suc n-1)} m≥n = begin-equality
   1 + (div-helper 0 n-1 (m ∸ n) n-1) ≡⟨⟩
   1 + (m ∸ n) / n                    ∎
 
+[m∸n]/n≡m/n∸1 : ∀ m n .{{_ : NonZero n}} → (m ∸ n) / n ≡ pred (m / n)
+[m∸n]/n≡m/n∸1 m n with <-≤-connex m n
+... | inj₁ m<n = begin-equality
+  (m ∸ n) / n  ≡⟨ m<n⇒m/n≡0 (≤-<-trans (m∸n≤m m n) m<n) ⟩
+  0            ≡⟨⟩
+  pred 0       ≡⟨ cong pred (m<n⇒m/n≡0 m<n) ⟨
+  pred (m / n) ∎
+... | inj₂ n≥m = begin-equality
+  (m ∸ n) / n            ≡⟨⟩
+  pred (1 + (m ∸ n) / n) ≡⟨ cong pred (m/n≡1+[m∸n]/n n≥m) ⟨
+  pred (m / n)           ∎
+
+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@.(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 ⟩
+  o % m                    ∎
+  where
+  pm = p * m
+
+  lem : o / pm * p * m ≤ o
+  lem = begin
+    o / pm * p * m       ≡⟨ *-assoc (o / pm) p m ⟩
+    o / pm * pm          ≤⟨ m/n*n≤m o pm ⟩
+    o                    ∎
+
 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 _) n o = helper (<-wellFounded n)
+m*n/m*o≡n/o m n o = helper (<-wellFounded n)
   where
+  instance _ = m*n≢0 m o
   helper : ∀ {n} → Acc _<_ n → (m * n) / (m * o) ≡ n / o
-  helper {n} (acc rec) with n <? o
-  ... | yes n<o = trans (m<n⇒m/n≡0 (*-monoʳ-< m n<o)) (sym (m<n⇒m/n≡0 n<o))
-  ... | no  n≮o = begin-equality
-    (m * n) / (m * o)             ≡⟨  m/n≡1+[m∸n]/n (*-monoʳ-≤ m (≮⇒≥ n≮o)) ⟩
-    1 + (m * n ∸ m * o) / (m * o) ≡⟨ cong (λ v → 1 + v / (m * o)) (*-distribˡ-∸ m n o) ⟨
-    1 + (m * (n ∸ o)) / (m * o)   ≡⟨  cong suc (helper (rec n∸o<n)) ⟩
-    1 + (n ∸ o) / o               ≡⟨ cong₂ _+_ (n/n≡1 o) refl ⟨
-    o / o + (n ∸ o) / o           ≡⟨ +-distrib-/-∣ˡ (n ∸ o) (divides 1 ((sym (*-identityˡ o)))) ⟨
-    (o + (n ∸ o)) / o             ≡⟨  cong (_/ o) (m+[n∸m]≡n (≮⇒≥ n≮o)) ⟩
+  helper {n} (acc rec) with <-≤-connex n o
+  ... | inj₁ n<o = trans (m<n⇒m/n≡0 (*-monoʳ-< m n<o)) (sym (m<n⇒m/n≡0 n<o))
+    where instance _ = m*n≢0⇒m≢0 m
+  ... | inj₂ n≥o = begin-equality
+    (m * n) / (m * o)             ≡⟨ m/n≡1+[m∸n]/n (*-monoʳ-≤ m n≥o) ⟩
+    1 + (m * n ∸ m * o) / (m * o) ≡⟨ cong (suc ∘ (_/ (m * o))) (*-distribˡ-∸ m n o) ⟨
+    1 + (m * (n ∸ o)) / (m * o)   ≡⟨ cong suc (helper (rec n∸o<n)) ⟩
+    1 + (n ∸ o) / o               ≡⟨ m/n≡1+[m∸n]/n n≥o ⟨
     n / o                         ∎
-    where n∸o<n = ∸-monoʳ-< (n≢0⇒n>0 (≢-nonZero⁻¹ o)) (≮⇒≥ n≮o)
+    where n∸o<n = ∸-monoʳ-< (n≢0⇒n>0 (≢-nonZero⁻¹ o)) n≥o
 
-m*n/o*n≡m/o : ∀ m n o .⦃ _ : NonZero o ⦄ ⦃ _ : NonZero (o * n) ⦄ →
+m*n/o*n≡m/o : ∀ m n o .{{_ : NonZero o}} .{{_ : NonZero (o * n)}} →
               m * n / (o * n) ≡ m / o
-m*n/o*n≡m/o m n o ⦃ _ ⦄ ⦃ o*n≢0 ⦄ = begin-equality
+m*n/o*n≡m/o m n o = begin-equality
   m * n / (o * n) ≡⟨ /-congˡ (*-comm m n) ⟩
   n * m / (o * n) ≡⟨ /-congʳ (*-comm o n) ⟩
   n * m / (n * o) ≡⟨ m*n/m*o≡n/o n m o ⟩
   m / o           ∎
-  where instance n*o≢0 = subst NonZero (*-comm o n) o*n≢0
-
-m<n*o⇒m/o<n : ∀ {m n o} .⦃ _ : NonZero o ⦄ → m < n * o → m / o < n
-m<n*o⇒m/o<n {m} {suc n} {o} m<n*o with m <? o
-... | yes m<o = begin-strict
+  where instance
+    _ : NonZero n
+    _ = m*n≢0⇒n≢0 o
+    _ : NonZero (n * o)
+    _ = m*n≢0 n o
+
+m<n*o⇒m/o<n : ∀ {m n o} .{{_ : NonZero o}} → m < n * o → m / o < n
+m<n*o⇒m/o<n {m} {1} {o} m<o rewrite *-identityˡ o = begin-strict
   m / o ≡⟨ m<n⇒m/n≡0 m<o ⟩
   0     <⟨ z<s ⟩
-  suc n ∎
-... | no m≮o = begin-strict
-  m / o             ≡⟨ m/n≡1+[m∸n]/n (≮⇒≥ m≮o) ⟩
-  suc ((m ∸ o) / o) <⟨ s≤s (m<n*o⇒m/o<n lem) ⟩
-  suc n             ∎
-  where
-  lem : m ∸ o < n * o
-  lem = begin-strict
-    m ∸ o         <⟨ ∸-monoˡ-< m<n*o (≮⇒≥ m≮o) ⟩
-    o + n * o ∸ o ≡⟨ m+n∸m≡n o (n * o) ⟩
-    n * o         ∎
-
-[m∸n]/n≡m/n∸1 : ∀ m n .⦃ _ : NonZero n ⦄ → (m ∸ n) / n ≡ pred (m / n)
-[m∸n]/n≡m/n∸1 m n with m <? n
-... | yes m<n = begin-equality
-  (m ∸ n) / n  ≡⟨ m<n⇒m/n≡0 (≤-<-trans (m∸n≤m m n) m<n) ⟩
-  0            ≡⟨⟩
-  0 ∸ 1        ≡⟨ cong (_∸ 1) (m<n⇒m/n≡0 m<n) ⟨
-  m / n ∸ 1    ≡⟨⟩
-  pred (m / n) ∎
-... | no m≮n = begin-equality
-  (m ∸ n) / n           ≡⟨⟩
-  suc ((m ∸ n) / n) ∸ 1 ≡⟨ cong (_∸ 1) (m/n≡1+[m∸n]/n (≮⇒≥ m≮n)) ⟨
-  m / n ∸ 1             ≡⟨⟩
-  pred (m / n)          ∎
-
-[m∸n*o]/o≡m/o∸n : ∀ m n o .⦃ _ : NonZero o ⦄ → (m ∸ n * o) / o ≡ m / o ∸ n
+  1 ∎
+m<n*o⇒m/o<n {m} {suc n@(suc _)} {o} m<n*o = pred-cancel-< $ begin-strict
+  pred (m / o) ≡⟨ [m∸n]/n≡m/n∸1 m o ⟨
+  (m ∸ o) / o  <⟨ m<n*o⇒m/o<n (m<n+o⇒m∸n<o m o m<n*o) ⟩
+  n ∎
+  where instance _ = m*n≢0 n o
+
+[m∸n*o]/o≡m/o∸n : ∀ m n o .{{_ : NonZero o}} → (m ∸ n * o) / o ≡ m / o ∸ n
 [m∸n*o]/o≡m/o∸n m zero    o = refl
 [m∸n*o]/o≡m/o∸n m (suc n) o = begin-equality
   (m ∸ (o + n * o)) / o ≡⟨ /-congˡ (∸-+-assoc m o (n * o)) ⟨
@@ -351,8 +357,8 @@ m<n*o⇒m/o<n {m} {suc n} {o} m<n*o with m <? o
   m / o ∸ 1 ∸ n         ≡⟨ ∸-+-assoc (m / o) 1 n ⟩
   m / o ∸ suc n         ∎
 
-m/n/o≡m/[n*o] : ∀ m n o .⦃ _ : NonZero n ⦄ .⦃ _ : NonZero o ⦄
-                .⦃ _ : NonZero (n * o) ⦄ → m / n / o ≡ m / (n * o)
+m/n/o≡m/[n*o] : ∀ m n o .{{_ : NonZero n}} .{{_ : NonZero o}}
+                .{{_ : NonZero (n * o)}} → m / n / o ≡ m / (n * o)
 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₁) ⟩
@@ -385,27 +391,34 @@ m/n/o≡m/[n*o] m n o = begin-equality
     o*n     ∎
 
 *-/-assoc : ∀ m {n d} .{{_ : NonZero d}} → d ∣ n → m * n / d ≡ m * (n / d)
-*-/-assoc zero    {_} {d@(suc _)} d∣n = 0/n≡0 (suc d)
-*-/-assoc (suc m) {n} {d@(suc _)} d∣n = begin-equality
+*-/-assoc zero    {_} {d} d∣n = 0/n≡0 d
+*-/-assoc (suc m) {n} {d} d∣n = begin-equality
   (n + m * n) / d     ≡⟨ +-distrib-/-∣ˡ _ d∣n ⟩
   n / d + (m * n) / d ≡⟨ cong (n / d +_) (*-/-assoc m d∣n) ⟩
   n / d + m * (n / d) ∎
 
-/-*-interchange : ∀ {m n o p} .{{_ : NonZero o}} .{{_ : NonZero p}} .{{_ : NonZero (o * p)}} →
+/-*-interchange : .{{_ : NonZero o}} .{{_ : NonZero p}} .{{_ : NonZero (o * p)}} →
                   o ∣ m → p ∣ n → (m * n) / (o * p) ≡ (m / o) * (n / p)
-/-*-interchange {m} {n} {o@(suc _)} {p@(suc _)} o∣m p∣n = *-cancelˡ-≡ _ _ (o * p) (begin-equality
-  (o * p) * ((m * n) / (o * p)) ≡⟨  m*[n/m]≡n (*-pres-∣ o∣m p∣n) ⟩
-  m * n                         ≡⟨ cong₂ _*_ (m*[n/m]≡n o∣m) (m*[n/m]≡n p∣n) ⟨
-  (o * (m / o)) * (p * (n / p)) ≡⟨ [m*n]*[o*p]≡[m*o]*[n*p] o (m / o) p (n / p) ⟩
-  (o * p) * ((m / o) * (n / p)) ∎)
+/-*-interchange {o} {p} {m@.(q * o)} {n@.(r * p)} (divides-refl q) (divides-refl r)
+  = begin-equality
+  (m * n) / (o * p) ≡⟨⟩
+  q * o * (r * p) / (o * p) ≡⟨ /-congˡ ([m*n]*[o*p]≡[m*o]*[n*p] q o r p) ⟩
+  q * r * (o * p) / (o * p) ≡⟨ m*n/n≡m (q * r) (o * p) ⟩
+  q * r                     ≡⟨ cong₂ _*_ (m*n/n≡m q o) (m*n/n≡m r p) ⟨
+  (q * o / o) * (r * p / p) ≡⟨⟩
+  (m / o) * (n / p)         ∎
 
 m*n/m!≡n/[m∸1]! : ∀ m n .{{_ : NonZero m}} →
-                 (m * n / m !) {{m !≢0}}  ≡ (n / (pred m) !) {{pred m !≢0}}
-m*n/m!≡n/[m∸1]! (suc m) n = m*n/m*o≡n/o (suc m) n (m !) {{m !≢0}} {{suc m !≢0}}
-
-m%[n*o]/o≡m/o%n : ∀ m n o .⦃ _ : NonZero n ⦄ .⦃ _ : NonZero o ⦄
-                  ⦃ _ : NonZero (n * o) ⦄ → m % (n * o) / o ≡ m / o % n
-m%[n*o]/o≡m/o%n m n o ⦃ _ ⦄ ⦃ _ ⦄ ⦃ n*o≢0 ⦄ = begin-equality
+                  let instance _ = m !≢0 ; instance _ = (pred m) !≢0 in
+                  (m * n / m !) ≡ (n / (pred m) !)
+m*n/m!≡n/[m∸1]! m′@(suc m) n = m*n/m*o≡n/o m′ n (m !)
+  where instance
+    _ = m !≢0
+    _ = m′ !≢0
+
+m%[n*o]/o≡m/o%n : ∀ m n o .{{_ : NonZero n}} .{{_ : NonZero o}} →
+                  {{_ : NonZero (n * o)}} → m % (n * o) / o ≡ m / o % n
+m%[n*o]/o≡m/o%n m n o = begin-equality
   m % (n * o) / o                   ≡⟨ /-congˡ (m%n≡m∸m/n*n m (n * o)) ⟩
   (m ∸ (m / (n * o) * (n * o))) / o ≡⟨ cong (λ # → (m ∸ #) / o) (*-assoc (m / (n * o)) n o) ⟨
   (m ∸ (m / (n * o) * n * o)) / o   ≡⟨ [m∸n*o]/o≡m/o∸n m (m / (n * o) * n) o ⟩
@@ -413,11 +426,11 @@ m%[n*o]/o≡m/o%n m n o ⦃ _ ⦄ ⦃ _ ⦄ ⦃ n*o≢0 ⦄ = begin-equality
   m / o ∸ m / (o * n) * n           ≡⟨ cong (λ # → m / o ∸ # * n) (m/n/o≡m/[n*o] m o n ) ⟨
   m / o ∸ m / o / n * n             ≡⟨ m%n≡m∸m/n*n (m / o) n ⟨
   m / o % n                         ∎
-  where instance o*n≢0 = subst NonZero (*-comm n o) n*o≢0
+  where instance _ = m*n≢0 o n
 
-m%n*o≡m*o%[n*o] : ∀ m n o .⦃ _ : NonZero n ⦄ ⦃ _ : NonZero (n * o) ⦄ →
+m%n*o≡m*o%[n*o] : ∀ m n o .{{_ : NonZero n}} .{{_ : NonZero (n * o)}} →
                   m % n * o ≡ m * o % (n * o)
-m%n*o≡m*o%[n*o] m n o ⦃ _ ⦄ ⦃ n*o≢0 ⦄ = begin-equality
+m%n*o≡m*o%[n*o] m n o = begin-equality
   m % n * o                         ≡⟨ cong (_* o) (m%n≡m∸m/n*n m n) ⟩
   (m ∸ m / n * n) * o               ≡⟨ *-distribʳ-∸ o m (m / n * n) ⟩
   m * o ∸ m / n * n * o             ≡⟨ cong (λ # → m * o ∸ # * n * o) (m*n/o*n≡m/o m o n) ⟨
@@ -425,9 +438,9 @@ m%n*o≡m*o%[n*o] m n o ⦃ _ ⦄ ⦃ n*o≢0 ⦄ = begin-equality
   m * o ∸ m * o / (n * o) * (n * o) ≡⟨ m%n≡m∸m/n*n (m * o) (n * o) ⟨
   m * o % (n * o)                   ∎
 
-[m*n+o]%[p*n]≡[m*n]%[p*n]+o : ∀ m {n o} p ⦃ _ : NonZero (p * n) ⦄ → o < n →
+[m*n+o]%[p*n]≡[m*n]%[p*n]+o : ∀ m {n o} p .{{_ : NonZero (p * n)}} → o < n →
                               (m * n + o) % (p * n) ≡ (m * n) % (p * n) + o
-[m*n+o]%[p*n]≡[m*n]%[p*n]+o m {n} {o} p@(suc p-1) ⦃ p*n≢0 ⦄ o<n = begin-equality
+[m*n+o]%[p*n]≡[m*n]%[p*n]+o m {n} {o} p@(suc p-1) o<n = begin-equality
   (mn + o) % pn           ≡⟨ %-distribˡ-+ mn o pn ⟩
   (mn % pn + o % pn) % pn ≡⟨ cong (λ # → (mn % pn + #) % pn) (m<n⇒m%n≡m (m<n⇒m<o*n p o<n)) ⟩
   (mn % pn + o) % pn      ≡⟨ m<n⇒m%n≡m lem₂ ⟩
@@ -458,6 +471,10 @@ record DivMod (dividend divisor : ℕ) : Set where
     remainder : Fin divisor
     property  : dividend ≡ toℕ remainder + quotient * divisor
 
+  nonZeroDivisor : NonZero divisor
+  nonZeroDivisor = nonZeroIndex remainder
+
+
 infixl 7 _div_ _mod_ _divMod_
 
 _div_ : (dividend divisor : ℕ) .{{_ : NonZero divisor}} → ℕ
diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda
index 9083642f80..abac2915a7 100644
--- a/src/Data/Nat/Divisibility.agda
+++ b/src/Data/Nat/Divisibility.agda
@@ -8,11 +8,11 @@
 
 module Data.Nat.Divisibility where
 
-open import Algebra
 open import Data.Nat.Base
 open import Data.Nat.DivMod
+  using (m≡m%n+[m/n]*n; m%n≡m∸m/n*n; m*n/n≡m; m*n%n≡0; *-/-assoc)
 open import Data.Nat.Properties
-open import Function.Base using (_∘′_; _$_)
+open import Function.Base using (_∘′_; _$_; flip)
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Level using (0ℓ)
 open import Relation.Nullary.Decidable as Dec using (yes; no)
@@ -25,24 +25,62 @@ open import Relation.Binary.Definitions
   using (Reflexive; Transitive; Antisymmetric; Decidable)
 import Relation.Binary.Reasoning.Preorder as PreorderReasoning
 open import Relation.Binary.PropositionalEquality.Core
-  using (_≡_; _≢_; refl; sym; trans; cong; cong₂; subst)
+  using (_≡_; _≢_; refl; sym; cong; subst)
 open import Relation.Binary.Reasoning.Syntax
-import Relation.Binary.PropositionalEquality.Properties as PropEq
+open import Relation.Binary.PropositionalEquality.Properties
+  using (isEquivalence; module ≡-Reasoning)
+
+private
+  variable d m n o p : ℕ
+
 
 ------------------------------------------------------------------------
--- Definition
+-- Definition and derived properties
+
+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≡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>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 ⟩
+    m * quotient m∣n ∎
+  where open ≤-Reasoning
 
-open import Data.Nat.Divisibility.Core public
+quotient-< : (m∣n : m ∣ n) → .{{NonTrivial m}} → .{{NonZero n}} → quotient m∣n < n
+quotient-< {m} {n} m∣n = begin-strict
+  quotient m∣n     <⟨ m<m*n (quotient m∣n) m (nonTrivial⇒n>1 m) ⟩
+  quotient m∣n * m ≡⟨ _∣_.equality m∣n ⟨
+  n                ∎
+  where open ≤-Reasoning; instance _ = quotient≢0 m∣n
+
+------------------------------------------------------------------------
+-- Relating _/_ and quotient
+
+n/m≡quotient : (m∣n : m ∣ n) .{{_ : NonZero m}} → n / m ≡ quotient m∣n
+n/m≡quotient {m = m} (divides-refl q) = m*n/n≡m q m
 
 ------------------------------------------------------------------------
 -- Relationship with _%_
 
 m%n≡0⇒n∣m : ∀ m n .{{_ : NonZero n}} → m % n ≡ 0 → n ∣ m
-m%n≡0⇒n∣m m n eq = divides (m / n) (begin-equality
-  m                  ≡⟨ m≡m%n+[m/n]*n m n ⟩
-  m % n + m / n * n  ≡⟨ cong₂ _+_ eq refl ⟩
-  m / n * n          ∎)
-  where open ≤-Reasoning
+m%n≡0⇒n∣m m n eq = divides (m / n) $ begin
+  m                ≡⟨ m≡m%n+[m/n]*n m n ⟩
+  m % n + [m/n]*n  ≡⟨ cong (_+ [m/n]*n) eq ⟩
+  [m/n]*n          ∎
+  where open ≡-Reasoning; [m/n]*n = m / n * n
 
 n∣m⇒m%n≡0 : ∀ m n .{{_ : NonZero n}} → n ∣ m → m % n ≡ 0
 n∣m⇒m%n≡0 .(q * n) n (divides-refl q) = m*n%n≡0 q n
@@ -53,15 +91,11 @@ m%n≡0⇔n∣m m n = mk⇔ (m%n≡0⇒n∣m m n) (n∣m⇒m%n≡0 m n)
 ------------------------------------------------------------------------
 -- Properties of _∣_ and _≤_
 
-∣⇒≤ : ∀ {m n} .{{_ : NonZero n}} → m ∣ n → m ≤ n
-∣⇒≤ {m} {n@(suc _)} (divides (suc q) eq) = begin
-  m          ≤⟨ m≤m+n m (q * m) ⟩
-  suc q * m  ≡⟨ sym eq ⟩
-  n          ∎
-  where open ≤-Reasoning
+∣⇒≤ : .{{_ : NonZero n}} → m ∣ n → m ≤ n
+∣⇒≤ {n@.(q * m)} {m} (divides-refl q@(suc p)) = m≤m+n m (p * m)
 
->⇒∤ : ∀ {m n} .{{_ : NonZero n}} → m > n → m ∤ n
->⇒∤ (s≤s m>n) m∣n = contradiction (∣⇒≤ m∣n) (≤⇒≯ m>n)
+>⇒∤ : .{{_ : NonZero n}} → m > n → m ∤ n
+>⇒∤ {n@(suc _)} n<m@(s<s _) m∣n = contradiction (∣⇒≤ m∣n) (<⇒≱ n<m)
 
 ------------------------------------------------------------------------
 -- _∣_ is a partial order
@@ -79,20 +113,20 @@ 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}  _ (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)
+∣-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 _∣?_
 
 _∣?_ : Decidable _∣_
 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)
+n@(suc _) ∣? m  = Dec.map (m%n≡0⇔n∣m m n) (m % n ≟ 0)
 
 ∣-isPreorder : IsPreorder _≡_ _∣_
 ∣-isPreorder = record
-  { isEquivalence = PropEq.isEquivalence
+  { isEquivalence = isEquivalence
   ; reflexive     = ∣-reflexive
   ; trans         = ∣-trans
   }
@@ -125,42 +159,43 @@ module ∣-Reasoning where
 
   open ∣-syntax _IsRelatedTo_ _IsRelatedTo_ ∣-go public
 
+
 ------------------------------------------------------------------------
 -- Simple properties of _∣_
 
-infix 10 1∣_ _∣0
-
-1∣_ : ∀ n → 1 ∣ n
-1∣ n = divides n (sym (*-identityʳ n))
+infix 10 _∣0 1∣_
 
 _∣0 : ∀ n → n ∣ 0
 n ∣0 = divides-refl 0
 
-0∣⇒≡0 : ∀ {n} → 0 ∣ n → n ≡ 0
+0∣⇒≡0 : 0 ∣ n → n ≡ 0
 0∣⇒≡0 {n} 0∣n = ∣-antisym (n ∣0) 0∣n
 
-∣1⇒≡1 : ∀ {n} → n ∣ 1 → n ≡ 1
+1∣_ : ∀ n → 1 ∣ n
+1∣ n = divides n (sym (*-identityʳ n))
+
+∣1⇒≡1 : n ∣ 1 → n ≡ 1
 ∣1⇒≡1 {n} n∣1 = ∣-antisym n∣1 (1∣ n)
 
-n∣n : ∀ {n} → n ∣ n
-n∣n {n} = ∣-refl
+n∣n : n ∣ 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 : d ∣ m → d ∣ n → d ∣ m + n
 ∣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
-∣m+n∣m⇒∣n {i} {m} {n} (divides p m+n≡p*i) (divides q m≡q*i) =
+∣m+n∣m⇒∣n : d ∣ m + n → d ∣ m → d ∣ n
+∣m+n∣m⇒∣n {d} {m} {n} (divides p m+n≡p*d) (divides-refl q) =
   divides (p ∸ q) $ begin-equality
-    n             ≡⟨ sym (m+n∸n≡m n m) ⟩
+    n             ≡⟨ m+n∸n≡m n m ⟨
     n + m ∸ m     ≡⟨ cong (_∸ m) (+-comm n m) ⟩
-    m + n ∸ m     ≡⟨ cong₂ _∸_ m+n≡p*i m≡q*i ⟩
-    p * i ∸ q * i ≡⟨ sym (*-distribʳ-∸ i p q) ⟩
-    (p ∸ q) * i   ∎
-  where open ∣-Reasoning
+    m + n ∸ m     ≡⟨ cong (_∸ m) m+n≡p*d ⟩
+    p * d ∸ q * d ≡⟨ *-distribʳ-∸ d p q ⟨
+    (p ∸ q) * d   ∎
+    where open ∣-Reasoning
 
 ------------------------------------------------------------------------
 -- Properties of _∣_ and _*_
@@ -174,99 +209,91 @@ m∣m*n n = divides n (*-comm _ n)
 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-refl q) = ∣-trans (n∣m*n q) (m∣m*n n)
+∣m⇒∣m*n : ∀ n → d ∣ m → d ∣ m * n
+∣m⇒∣m*n 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} → d ∣ n → d ∣ 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 → m * n ∣ d → m ∣ d
 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 → m * n ∣ d → n ∣ d
 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@.(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 ⟩
-  q * (k * i)  ∎
-  where open ≤-Reasoning
+*-pres-∣ : o ∣ m → p ∣ n → o * p ∣ m * n
+*-pres-∣ {o} {m@.(q * o)} {p} {n@.(r * p)} (divides-refl q) (divides-refl r) =
+  divides (q * r) ([m*n]*[o*p]≡[m*o]*[n*p] q o r p)
 
-*-monoˡ-∣ : ∀ {i j} k → i ∣ j → i * k ∣ j * k
-*-monoˡ-∣ {i} {j} k rewrite *-comm i k | *-comm j k = *-monoʳ-∣ k
+*-monoʳ-∣ : ∀ o → m ∣ n → o * m ∣ o * n
+*-monoʳ-∣ o = *-pres-∣ (∣-refl {o})
 
-*-cancelˡ-∣ : ∀ {i j} k .{{_ : NonZero k}} → k * i ∣ k * j → i ∣ j
-*-cancelˡ-∣ {i} {j} k@(suc _) (divides q eq) =
-  divides q $ *-cancelʳ-≡ j (q * i) _ $ begin-equality
-    j * k        ≡⟨ *-comm j k ⟩
-    k * j        ≡⟨ eq ⟩
-    q * (k * i)  ≡⟨ cong (q *_) (*-comm k i) ⟩
-    q * (i * k)  ≡⟨ sym (*-assoc q i k) ⟩
-    (q * i) * k  ∎
-    where open ≤-Reasoning
+*-monoˡ-∣ : ∀ o → m ∣ n → m * o ∣ n * o
+*-monoˡ-∣ o = flip *-pres-∣ (∣-refl {o})
+
+*-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 * m * q   ≡⟨ *-assoc o m q ⟩
+  o * (m * q) ≡⟨ cong (o *_) (*-comm q m) ⟨
+  o * (q * m) ∎
+  where
+  open ∣-Reasoning
+  q = quotient o*m∣o*n
 
-*-cancelʳ-∣ : ∀ {i j} k .{{_ : NonZero k}} → i * k ∣ j * k → i ∣ j
-*-cancelʳ-∣ {i} {j} k rewrite *-comm i k | *-comm j k = *-cancelˡ-∣ k
+*-cancelʳ-∣ : ∀ o .{{_ : NonZero o}} → m * o ∣ n * o → m ∣ n
+*-cancelʳ-∣ {m} {n} o rewrite *-comm m o | *-comm n o = *-cancelˡ-∣ o
 
 ------------------------------------------------------------------------
 -- Properties of _∣_ and _∸_
 
-∣m∸n∣n⇒∣m : ∀ i {m n} → n ≤ m → i ∣ m ∸ n → i ∣ n → i ∣ m
-∣m∸n∣n⇒∣m i {m} {n} n≤m (divides p m∸n≡p*i) (divides q n≡q*o) =
+∣m∸n∣n⇒∣m : ∀ d → n ≤ m → d ∣ m ∸ n → d ∣ n → d ∣ m
+∣m∸n∣n⇒∣m {n} {m} d n≤m (divides p m∸n≡p*d) (divides-refl q) =
   divides (p + q) $ begin-equality
-    m             ≡⟨ sym (m+[n∸m]≡n n≤m) ⟩
+    m             ≡⟨ m+[n∸m]≡n n≤m ⟨
     n + (m ∸ n)   ≡⟨ +-comm n (m ∸ n) ⟩
-    m ∸ n + n     ≡⟨ cong₂ _+_ m∸n≡p*i n≡q*o ⟩
-    p * i + q * i ≡⟨ sym (*-distribʳ-+ i p q)  ⟩
-    (p + q) * i   ∎
-  where open ≤-Reasoning
+    m ∸ n + n     ≡⟨ cong (_+ n) m∸n≡p*d ⟩
+    p * d + q * d ≡⟨ *-distribʳ-+ d p q ⟨
+    (p + q) * d   ∎
+  where open ∣-Reasoning
 
 ------------------------------------------------------------------------
 -- Properties of _∣_ and _/_
 
-m/n∣m : ∀ {m n} .{{_ : NonZero n}} → n ∣ m → m / n ∣ m
-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     ≡⟨⟩
-  m         ∎
+m/n∣m : .{{_ : NonZero n}} → n ∣ m → m / n ∣ m
+m/n∣m {n} {m} n∣m = begin
+  m / n        ≡⟨ n/m≡quotient n∣m ⟩
+  quotient n∣m ∣⟨ quotient-∣ n∣m ⟩
+  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 {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 ≡⟨⟩
-  o / n           ∎
+m*n∣o⇒m∣o/n : ∀ m n .{{_ : NonZero n}} → m * n ∣ o → m ∣ o / n
+m*n∣o⇒m∣o/n m n (divides-refl p) = divides p $ begin-equality
+  p * (m * n) / n   ≡⟨ *-/-assoc p (n∣m*n m) ⟩
+  p * ((m * n) / n) ≡⟨ cong (p *_) (m*n/n≡m m n) ⟩
+  p * m ∎
   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 .{{_ : 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-refl p) m∣p*o/o = begin
+m∣n/o⇒m*o∣n : .{{_ : NonZero o}} → o ∣ n → m ∣ n / o → m * o ∣ n
+m∣n/o⇒m*o∣n {o} {n@.(p * o)} {m} (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
 
-m∣n/o⇒o*m∣n : ∀ {m n o} .{{_ : NonZero o}} → o ∣ n → m ∣ n / o → o * m ∣ n
-m∣n/o⇒o*m∣n {m} {_} {o} rewrite *-comm o m = m∣n/o⇒m*o∣n
+m∣n/o⇒o*m∣n : .{{_ : NonZero o}} → o ∣ n → m ∣ n / o → o * m ∣ n
+m∣n/o⇒o*m∣n {o} {_} {m} 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-refl p) p*n/n∣o = begin
+m/n∣o⇒m∣o*n : .{{_ : NonZero n}} → n ∣ m → m / n ∣ o → m ∣ o * n
+m/n∣o⇒m∣o*n {n} {m@.(p * 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 {m@.(p * n)} {n@(suc _)} {o} (divides-refl p) pn∣on = begin
+m∣n*o⇒m/n∣o : .{{_ : NonZero n}} → n ∣ m → m ∣ o * n → m / n ∣ o
+m∣n*o⇒m/n∣o {n} {m@.(p * n)} {o} (divides-refl p) pn∣on = begin
   m / n     ≡⟨⟩
   p * n / n ≡⟨ m*n/n≡m p n ⟩
   p         ∣⟨ *-cancelʳ-∣ n pn∣on ⟩
@@ -276,58 +303,58 @@ m∣n*o⇒m/n∣o {m@.(p * n)} {n@(suc _)} {o} (divides-refl p) 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@.(a * d)} {d} (divides-refl a) (divides b m%n≡bd) =
-  divides (b + (m / n) * a) (begin-equality
+∣n∣m%n⇒∣m : .{{_ : NonZero n}} → d ∣ n → d ∣ m % n → d ∣ m
+∣n∣m%n⇒∣m {n@.(p * d)} {d} {m} (divides-refl p) (divides q m%n≡qd) =
+  divides (q + (m / n) * p) $ begin-equality
     m                         ≡⟨ m≡m%n+[m/n]*n m n ⟩
-    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@.(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
+    m % n + (m / n) * n       ≡⟨ cong (_+ (m / n) * n) m%n≡qd ⟩
+    q * d + (m / n) * n       ≡⟨⟩
+    q * d + (m / n) * (p * d) ≡⟨ cong (q * d +_) (*-assoc (m / n) p d) ⟨
+    q * d + ((m / n) * p) * d ≡⟨ *-distribʳ-+ d q _ ⟨
+    (q + (m / n) * p) * d     ∎
+  where open ∣-Reasoning
+
+%-presˡ-∣ : .{{_ : NonZero n}} → d ∣ m → d ∣ n → d ∣ m % n
+%-presˡ-∣ {n} {d} {m@.(p * d)} (divides-refl p) (divides q 1+n≡qd) =
+  divides (p ∸ m / n * q) $ begin-equality
+    m % n                   ≡⟨ m%n≡m∸m/n*n m n ⟩
+    m ∸ m / n * n           ≡⟨ cong (λ v → m ∸ m / n * v) 1+n≡qd ⟩
+    m ∸ m / n * (q * d)     ≡⟨ cong (m ∸_) (*-assoc (m / n) q d) ⟨
+    m  ∸ (m / n * q) * d    ≡⟨⟩
+    p * d ∸ (m / n * q) * d ≡⟨ *-distribʳ-∸ d p (m / n * q) ⟨
+    (p ∸ m / n * q) * d     ∎
+  where open ∣-Reasoning
 
 ------------------------------------------------------------------------
 -- Properties of _∣_ and !_
 
-m≤n⇒m!∣n! : ∀ {m n} → m ≤ n → m ! ∣ n !
+m≤n⇒m!∣n! : m ≤ n → m ! ∣ n !
 m≤n⇒m!∣n! m≤n = help (≤⇒≤′ m≤n)
   where
-  help : ∀ {m n} → m ≤′ n → m ! ∣ n !
-  help {m} {n}     ≤′-refl        = ∣-refl
-  help {m} {suc n} (≤′-step m≤′n) = ∣n⇒∣m*n (suc n) (help m≤′n)
+  help : m ≤′ n → m ! ∣ n !
+  help         ≤′-refl       = ∣-refl
+  help {n = n} (≤′-step m≤n) = ∣n⇒∣m*n n (help m≤n)
 
 ------------------------------------------------------------------------
--- Properties of _BoundedNonTrivialDivisor_
+-- Properties of _HasNonTrivialDivisorLessThan_
 
 -- Smart constructor
 
-hasNonTrivialDivisor-≢ : ∀ {d n} → .{{NonTrivial d}} → .{{NonZero n}} →
+hasNonTrivialDivisor-≢ : .{{NonTrivial d}} → .{{NonZero n}} →
                          d ≢ n → d ∣ n → n HasNonTrivialDivisorLessThan n
 hasNonTrivialDivisor-≢ d≢n d∣n
   = hasNonTrivialDivisor (≤∧≢⇒< (∣⇒≤ d∣n) d≢n) d∣n
 
 -- Monotonicity wrt ∣
 
-hasNonTrivialDivisor-∣ : ∀ {m n o} → m HasNonTrivialDivisorLessThan n → m ∣ o →
+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)
 
 -- Monotonicity wrt ≤
 
-hasNonTrivialDivisor-≤ : ∀ {m n o} → 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-≤ : m HasNonTrivialDivisorLessThan n → n ≤ o →
+                         m HasNonTrivialDivisorLessThan o
+hasNonTrivialDivisor-≤ (hasNonTrivialDivisor d<n d∣m) m≤o
+  = hasNonTrivialDivisor (<-≤-trans d<n m≤o) d∣m
diff --git a/src/Data/Nat/Divisibility/Core.agda b/src/Data/Nat/Divisibility/Core.agda
index 58ef913a5f..1b43ab22d6 100644
--- a/src/Data/Nat/Divisibility/Core.agda
+++ b/src/Data/Nat/Divisibility/Core.agda
@@ -14,11 +14,14 @@ module Data.Nat.Divisibility.Core where
 
 open import Data.Nat.Base using (ℕ; _*_; _<_; NonTrivial)
 open import Data.Nat.Properties
-open import Level using (0ℓ)
 open import Relation.Nullary.Negation using (¬_)
 open import Relation.Binary.Core using (Rel)
-open import Relation.Binary.PropositionalEquality
-  using (_≡_; refl; sym; cong₂; module ≡-Reasoning)
+open import Relation.Binary.PropositionalEquality.Core
+  using (_≡_; refl)
+
+
+private
+  variable m n o p : ℕ
 
 ------------------------------------------------------------------------
 -- Main definition
@@ -35,15 +38,16 @@ record _∣_ (m n : ℕ) : Set where
   constructor divides
   field quotient : ℕ
         equality : n ≡ quotient * m
-open _∣_ using (quotient) public
 
-_∤_ : Rel ℕ 0ℓ
+_∤_ : Rel ℕ _
 m ∤ n = ¬ (m ∣ n)
 
 -- Smart constructor
 
 pattern divides-refl q = divides q refl
 
+open _∣_ using (quotient) public
+
 ------------------------------------------------------------------------
 -- Restricted divisor relation
 
@@ -60,12 +64,18 @@ record _HasNonTrivialDivisorLessThan_ (m n : ℕ) : Set where
     divisor-∣       : divisor ∣ m
 
 ------------------------------------------------------------------------
--- Basic properties
-
-*-pres-∣ : ∀ {m n o p} → o ∣ m → p ∣ n → o * p ∣ m * n
-*-pres-∣ {m} {n} {o} {p} (divides c m≡c*o) (divides d n≡d*p) =
-  divides (c * d) (begin
-    m * n             ≡⟨ cong₂ _*_ m≡c*o n≡d*p ⟩
-    (c * o) * (d * p) ≡⟨ [m*n]*[o*p]≡[m*o]*[n*p] c o d p ⟩
-    (c * d) * (o * p) ∎)
-  where open ≡-Reasoning
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.1
+
+*-pres-∣ : o ∣ m → p ∣ n → o * p ∣ m * n
+*-pres-∣ {o} {m@.(q * o)} {p} {n@.(r * p)} (divides-refl q) (divides-refl r) =
+  divides (q * r) ([m*n]*[o*p]≡[m*o]*[n*p] q o r p)
+
+{-# WARNING_ON_USAGE *-pres-∣
+"Warning: *-pres-∣ was deprecated in v2.1.
+ Please use Data.Nat.Divisibility.*-pres-∣ instead."
+#-}
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index ab1678ac9b..b09b46db7d 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -908,7 +908,7 @@ m*n≡0⇒m≡0∨n≡0 : ∀ m {n} → m * n ≡ 0 → m ≡ 0 ⊎ n ≡ 0
 m*n≡0⇒m≡0∨n≡0 zero    {n}     eq = inj₁ refl
 m*n≡0⇒m≡0∨n≡0 (suc m) {zero}  eq = inj₂ refl
 
-m*n≢0 : ∀ m n → .{{_ : NonZero m}} .{{_ : NonZero n}} → NonZero (m * n)
+m*n≢0 : ∀ m n .{{_ : NonZero m}} .{{_ : NonZero n}} → NonZero (m * n)
 m*n≢0 (suc m) (suc n) = _
 
 m*n≢0⇒m≢0 : ∀ m {n} → .{{NonZero (m * n)}} → NonZero m
@@ -947,9 +947,9 @@ n≢0∧m>1⇒m*n>1 m n rewrite *-comm m n = m≢0∧n>1⇒m*n>1 n m
 -- Other properties of _*_ and _≤_/_<_
 
 *-cancelʳ-≤ : ∀ m n o .{{_ : NonZero o}} → m * o ≤ n * o → m ≤ n
-*-cancelʳ-≤ zero    _       (suc o) _  = z≤n
-*-cancelʳ-≤ (suc m) (suc n) (suc o) le =
-  s≤s (*-cancelʳ-≤ m n (suc o) (+-cancelˡ-≤ _ _ _ le))
+*-cancelʳ-≤ zero    _       _         _  = z≤n
+*-cancelʳ-≤ (suc m) (suc n) o@(suc _) le =
+  s≤s (*-cancelʳ-≤ m n o (+-cancelˡ-≤ _ _ _ le))
 
 *-cancelˡ-≤ : ∀ o .{{_ : NonZero o}} → o * m ≤ o * n → m ≤ n
 *-cancelˡ-≤ {m} {n} o rewrite *-comm o m | *-comm o n = *-cancelʳ-≤ m n o
@@ -969,14 +969,12 @@ n≢0∧m>1⇒m*n>1 m n rewrite *-comm m n = m≢0∧n>1⇒m*n>1 n m
 *-mono-< (s<s m<n@(s≤s _)) u<v@(s≤s _) = +-mono-< u<v (*-mono-< m<n u<v)
 
 *-monoˡ-< : ∀ n .{{_ : NonZero n}} → (_* n) Preserves _<_ ⟶ _<_
-*-monoˡ-< (suc n) z<s       = 0<1+n
-*-monoˡ-< (suc n) (s<s m<o@(s≤s _)) =
-  +-mono-≤-< (≤-refl {suc n}) (*-monoˡ-< (suc n) m<o)
+*-monoˡ-< n@(suc _) z<s               = 0<1+n
+*-monoˡ-< n@(suc _) (s<s m<o@(s≤s _)) = +-mono-≤-< ≤-refl (*-monoˡ-< n m<o)
 
 *-monoʳ-< : ∀ n .{{_ : NonZero n}} → (n *_) Preserves _<_ ⟶ _<_
 *-monoʳ-< (suc zero)      m<o@(s≤s _) = +-mono-≤ m<o z≤n
-*-monoʳ-< (suc n@(suc _)) m<o@(s≤s _) =
-  +-mono-≤ m<o (<⇒≤ (*-monoʳ-< n m<o))
+*-monoʳ-< (suc n@(suc _)) m<o@(s≤s _) = +-mono-≤ m<o (<⇒≤ (*-monoʳ-< n m<o))
 
 m≤m*n : ∀ m n .{{_ : NonZero n}} → m ≤ m * n
 m≤m*n m n@(suc _) = begin
@@ -1598,10 +1596,20 @@ m≤n⇒n∸m≤n (s≤s m≤n) = m≤n⇒m≤1+n (m≤n⇒n∸m≤n m≤n)
   (m + n) ∸ o          ≡⟨ +-∸-assoc m o≤n ⟩
   m + (n ∸ o)          ∎
 
-m+n≤o⇒m≤o∸n : ∀ m n o → m + n ≤ o → m ≤ o ∸ n
-m+n≤o⇒m≤o∸n zero    n o       le       = z≤n
-m+n≤o⇒m≤o∸n (suc m) n (suc o) (s≤s le)
-  rewrite +-∸-assoc 1 (m+n≤o⇒n≤o m le) = s≤s (m+n≤o⇒m≤o∸n m n o le)
+m≤n+o⇒m∸n≤o : ∀ m n {o} → m ≤ n + o → m ∸ n ≤ o
+m≤n+o⇒m∸n≤o      m  zero    le = le
+m≤n+o⇒m∸n≤o zero    (suc n)  _ = z≤n
+m≤n+o⇒m∸n≤o (suc m) (suc n) le = m≤n+o⇒m∸n≤o m n (s≤s⁻¹ le)
+
+m<n+o⇒m∸n<o : ∀ m n {o} → .{{NonZero o}} → m < n + o → m ∸ n < o
+m<n+o⇒m∸n<o      m  zero                lt = lt
+m<n+o⇒m∸n<o zero    (suc n) {o@(suc _)} lt = z<s
+m<n+o⇒m∸n<o (suc m) (suc n)             lt = m<n+o⇒m∸n<o m n  (s<s⁻¹ lt)
+
+m+n≤o⇒m≤o∸n : ∀ m {n o} → m + n ≤ o → m ≤ o ∸ n
+m+n≤o⇒m≤o∸n zero    le       = z≤n
+m+n≤o⇒m≤o∸n (suc m) (s≤s le)
+  rewrite +-∸-assoc 1 (m+n≤o⇒n≤o m le) = s≤s (m+n≤o⇒m≤o∸n m le)
 
 m≤o∸n⇒m+n≤o : ∀ m {n o} (n≤o : n ≤ o) → m ≤ o ∸ n → m + n ≤ o
 m≤o∸n⇒m+n≤o m         z≤n       le rewrite +-identityʳ m = le
@@ -1728,6 +1736,25 @@ pred-mono-≤ {suc _} {suc _} m≤n = s≤s⁻¹ m≤n
 pred-mono-< : .{{NonZero m}} → m < n → pred m < pred n
 pred-mono-< {m = suc _} {n = suc _} = s<s⁻¹
 
+pred-cancel-≤ : pred m ≤ pred n → (m ≡ 1 × n ≡ 0) ⊎ m ≤ n
+pred-cancel-≤ {m = zero}  {n = zero}  _  = inj₂ z≤n
+pred-cancel-≤ {m = zero}  {n = suc _} _  = inj₂ z≤n
+pred-cancel-≤ {m = suc _} {n = zero} z≤n = inj₁ (refl , refl)
+pred-cancel-≤ {m = suc _} {n = suc _} le = inj₂ (s≤s le)
+
+pred-cancel-< : pred m < pred n → m < n
+pred-cancel-< {m = zero}  {n = suc _} _ = z<s
+pred-cancel-< {m = suc _} {n = suc _}   = s<s
+
+pred-injective : .{{NonZero m}} → .{{NonZero n}} → pred m ≡ pred n → m ≡ n
+pred-injective {suc m} {suc n} = cong suc
+
+pred-cancel-≡ : pred m ≡ pred n → ((m ≡ 0 × n ≡ 1) ⊎ (m ≡ 1 × n ≡ 0)) ⊎ m ≡ n
+pred-cancel-≡ {m = zero}  {n = zero}  _    = inj₂ refl
+pred-cancel-≡ {m = zero}  {n = suc _} refl = inj₁ (inj₁ (refl , refl))
+pred-cancel-≡ {m = suc _} {n = zero}  refl = inj₁ (inj₂ (refl , refl))
+pred-cancel-≡ {m = suc _} {n = suc _}      = inj₂ ∘ pred-injective
+
 ------------------------------------------------------------------------
 -- Properties of ∣_-_∣
 ------------------------------------------------------------------------
diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index f0a7d11c96..6ff6a8bc6d 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -311,12 +311,12 @@ normalize-injective-≃ : ∀ m n c d {{_ : ℕ.NonZero c}} {{_ : ℕ.NonZero d}
 normalize-injective-≃ m n c d eq = ℕ./-cancelʳ-≡
   md∣gcd[m,c]gcd[n,d]
   nc∣gcd[m,c]gcd[n,d]
-  (begin
+  $ begin
     (m ℕ.* d) ℕ./ (gcd[m,c] ℕ.* gcd[n,d]) ≡⟨  ℕ./-*-interchange gcd[m,c]∣m gcd[n,d]∣d ⟩
     (m ℕ./ gcd[m,c]) ℕ.* (d ℕ./ gcd[n,d]) ≡⟨  cong₂ ℕ._*_ m/gcd[m,c]≡n/gcd[n,d] (sym c/gcd[m,c]≡d/gcd[n,d]) ⟩
     (n ℕ./ gcd[n,d]) ℕ.* (c ℕ./ gcd[m,c]) ≡⟨ ℕ./-*-interchange gcd[n,d]∣n gcd[m,c]∣c ⟨
-    (n ℕ.* c) ℕ./ (gcd[n,d] ℕ.* gcd[m,c]) ≡⟨  ℕ./-congʳ (ℕ.*-comm gcd[n,d] gcd[m,c]) ⟩
-    (n ℕ.* c) ℕ./ (gcd[m,c] ℕ.* gcd[n,d]) ∎)
+    (n ℕ.* c) ℕ./ (gcd[n,d] ℕ.* gcd[m,c]) ≡⟨ ℕ./-congʳ (ℕ.*-comm gcd[n,d] gcd[m,c]) ⟩
+    (n ℕ.* c) ℕ./ (gcd[m,c] ℕ.* gcd[n,d]) ∎
   where
   open ≡-Reasoning
   gcd[m,c]   = ℕ.gcd m c
@@ -331,14 +331,13 @@ normalize-injective-≃ m n c d eq = ℕ./-cancelʳ-≡
 
   gcd[m,c]≢0′          = ℕ.gcd[m,n]≢0 m c (inj₂ (ℕ.≢-nonZero⁻¹ c))
   gcd[n,d]≢0′          = ℕ.gcd[m,n]≢0 n d (inj₂ (ℕ.≢-nonZero⁻¹ d))
-  gcd[m,c]*gcd[n,d]≢0′ = Sum.[ gcd[m,c]≢0′ , gcd[n,d]≢0′ ] ∘ ℕ.m*n≡0⇒m≡0∨n≡0 _
   instance
     gcd[m,c]≢0   = ℕ.≢-nonZero gcd[m,c]≢0′
     gcd[n,d]≢0   = ℕ.≢-nonZero gcd[n,d]≢0′
     c/gcd[m,c]≢0 = ℕ.≢-nonZero (ℕ.n/gcd[m,n]≢0 m c {{gcd≢0 = gcd[m,c]≢0}})
     d/gcd[n,d]≢0 = ℕ.≢-nonZero (ℕ.n/gcd[m,n]≢0 n d {{gcd≢0 = gcd[n,d]≢0}})
-    gcd[m,c]*gcd[n,d]≢0 = ℕ.≢-nonZero gcd[m,c]*gcd[n,d]≢0′
-    gcd[n,d]*gcd[m,c]≢0 = ℕ.≢-nonZero (subst (_≢ 0) (ℕ.*-comm gcd[m,c] gcd[n,d]) gcd[m,c]*gcd[n,d]≢0′)
+    gcd[m,c]*gcd[n,d]≢0 = ℕ.m*n≢0 gcd[m,c] gcd[n,d]
+    gcd[n,d]*gcd[m,c]≢0 = ℕ.m*n≢0 gcd[n,d] gcd[m,c]
 
   div = mkℚ+-injective eq
   m/gcd[m,c]≡n/gcd[n,d] = proj₁ div