diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2d61629e75..a2dc41e278 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -270,6 +270,28 @@ Additions to existing modules
   _<ᵇ_ : ℤ → ℤ → Bool
   ```
 
+* In `Data.Integer.DivMod`:
+  ```agda
+  n<0⇒n/ℕd<0                : n < 0ℤ → (n /ℕ d) < 0ℤ
+  0/ℕd≡0                    : + 0 /ℕ d ≡ + 0
+  0/d≡0                     : + 0 / d ≡ + 0
+  n/ℕ1≡n                    : n /ℕ 1 ≡ n
+  n/1≡n                     : n / + 1 ≡ n
+  n/ℕd≡0⇒∣n∣<d              : n /ℕ d ≡ 0ℤ → ∣ n ∣ ℕ.< d
+  0≤n<d⇒n/ℕd≡0              : n < + d → n /ℕ d ≡ 0ℤ
+  n/d≡0⇒∣n∣<∣d∣             : n / d ≡ 0ℤ → ∣ n ∣ ℕ.< ∣ d ∣
+  0≤n<∣d∣⇒n/d≡0             : n < + ∣ d ∣ → n / d ≡ 0ℤ
+  /ℕ-monoˡ-≤                : Monotonic₁ _≤_ _≤_ (_/ℕ d)
+  /ℕ-monoʳ-≤-nonNeg         : d₁ ℕ.≤ d₂ → n /ℕ d₂ ≤ n /ℕ d₁
+  /ℕ-monoʳ-≤-nonPos         : d₁ ℕ.≤ d₂ → n /ℕ d₁ ≤ n /ℕ d₂
+  /-monoˡ-≤-pos             : Monotonic₁ _≤_ _≤_ (_/ d)
+  /-monoˡ-≤-neg             : Monotonic₁ _≤_ _≥_ (_/ d)
+  /-monoʳ-≤-nonNeg-eq-signs : {sign d₁ ≡ sign d₂} → d₁ ≤ d₂ → n / d₁ ≥ n / d₂
+  /-monoʳ-≤-nonPos-eq-signs : {sign d₁ ≡ sign d₂} → d₁ ≤ d₂ → n / d₁ ≤ n / d₂
+  /-monoʳ-≤-nonNeg-op-signs : {sign d₁ ≡ opposite (sign d₂)} → d₁ ≤ d₂ → n / d₁ ≤ n / d₂
+  /-monoʳ-≤-nonPos-op-signs : {sign d₁ ≡ opposite (sign d₂)} → d₁ ≤ d₂ → n / d₁ ≥ n / d₂
+  ```
+
 * In `Data.Integer.Properties`:
   ```
   <ᵇ⇒< : T (i <ᵇ j) → i < j
@@ -294,6 +316,13 @@ Additions to existing modules
   n≤o⇒m^n∣m^o : ∀ m → .(n ≤ o) → m ^ n ∣ m ^ o
   ```
 
+* In `Data.Nat.DivMod`:
+  ```agda
+  %-pred-≡suc        : suc m % d ≡ suc k → m % d ≡ k
+  sn%d≡0⇒sn/d≡s[n/d] : suc n % d ≡ 0 → suc n / d ≡ suc (n / d)
+  sn%d>0⇒sn/d≡n/d    : 0 < suc n % d → suc n / d ≡ n / d
+  ```
+
 * In `Data.Nat.Logarithm`
   ```agda
   2^⌊log₂n⌋≤n : ∀ n .{{ _ : NonZero n }} → 2 ^ ⌊log₂ n ⌋ ≤ n
@@ -360,11 +389,21 @@ Additions to existing modules
 
 * In `Data.Rational.Unnormalised.Properties`:
   ```agda
-  <ᵇ⇒<          : T (p <ᵇ q) → p < q
-  <⇒<ᵇ          : p < q → T (p <ᵇ q)
-  p*q≃0⇒p≃0∨q≃0 : p * q ≃ 0ℚᵘ → p ≃ 0ℚᵘ ⊎ q ≃ 0ℚᵘ
-  p*q≄0⇒p≄0     : p * q ≄ 0ℚᵘ → p ≄ 0ℚᵘ
-  p*q≢0⇒q≢0     : p * q ≄ 0ℚᵘ → q ≄ 0ℚᵘ
+  <ᵇ⇒<             : T (p <ᵇ q) → p < q
+  <⇒<ᵇ             : p < q → T (p <ᵇ q)
+  p*q≃0⇒p≃0∨q≃0    : p * q ≃ 0ℚᵘ → p ≃ 0ℚᵘ ⊎ q ≃ 0ℚᵘ
+  p*q≄0⇒p≄0        : p * q ≄ 0ℚᵘ → p ≄ 0ℚᵘ
+  p*q≢0⇒q≢0        : p * q ≄ 0ℚᵘ → q ≄ 0ℚᵘ
+  ↧ₙ[n/d]≡d        : ↧ₙ (n / d) ≡ d
+  n/d≡[n/1]*[1/d]  : n / d ≡ (n / 1) * (1ℤ / d)
+  n/d≃[n/a]*[a/d]  : n / d ≃ (n / a) * (ℤ.+ a / d)
+  /-distribʳ-+     : (n ℤ.+ m) / d ≃ n / d + m / d
+  /-monoˡ-<        : Monotonic₁ ℤ._<_ _<_ (_/ d)
+  /-monoʳ-<-pos    : d₁ ℕ.< d₂ → n / d₂ < n / d₁
+  /-monoʳ-<-neg    : d₁ ℕ.< d₂ → n / d₁ < n / d₂
+  /-monoˡ-≤        : Monotonic₁ ℤ._≤_ _≤_ (_/ d)
+  /-monoʳ-≤-nonNeg : d₁ ℕ.≤ d₂ → n / d₂ ≤ n / d₁
+  /-monoʳ-≤-nonPos : d₁ ℕ.≤ d₂ → n / d₁ ≤ n / d₂
   ```
 
 * In `Data.Rational.Unnormalised.Show`:
diff --git a/src/Data/Integer/DivMod.agda b/src/Data/Integer/DivMod.agda
index 4f4572d2eb..008884970b 100644
--- a/src/Data/Integer/DivMod.agda
+++ b/src/Data/Integer/DivMod.agda
@@ -8,16 +8,22 @@
 
 module Data.Integer.DivMod where
 
-open import Data.Integer.Base using (+_; -[1+_]; +[1+_]; NonZero; _%_; ∣_∣;
-  _%ℕ_; _/ℕ_; _+_; _*_; -_; _-_; pred; -1ℤ; 0ℤ; _⊖_; _≤_; _<_; +≤+; suc;
-  +<+)
+open import Data.Integer.Base using (+_; -[1+_]; +[1+_]; ∣_∣; _+_; _*_; -_;
+  _-_; suc; pred; -1ℤ; 0ℤ; _⊖_; _≤_; _≥_; _<_; +≤+; -≤-; -≤+; +<+; -<+;
+  NonZero; NonNegative; NonPositive; Negative; Positive; sign)
 open import Data.Integer.Properties
 open import Data.Nat.Base as ℕ using (ℕ; z≤n; s≤s; z<s; s<s)
-import Data.Nat.Properties as ℕ using (m∸n≤m)
-import Data.Nat.DivMod as ℕ using (m≡m%n+[m/n]*n; m%n≤n; m%n<n)
+import Data.Nat.Properties as ℕ using (≤-reflexive; m∸n≤m; m<n⇒0<n)
+import Data.Nat.DivMod as ℕ using (m≡m%n+[m/n]*n; m%n≤n; m%n<n; n/1≡n; n%1≡0;
+  m/n≡0⇒m<n; m<n⇒m/n≡0; sn%d≡0⇒sn/d≡s[n/d]; sn%d>0⇒sn/d≡n/d; /-monoˡ-≤;
+  /-monoʳ-≤; 0/n≡0)
+open import Data.Sign.Base using (opposite)
 open import Function.Base using (_∘′_)
-open import Relation.Binary.PropositionalEquality.Core
-  using (_≡_; cong; sym; subst)
+open import Relation.Binary.Definitions using (Monotonic₁)
+open import Relation.Binary.PropositionalEquality
+  using (_≡_; cong; sym; subst; trans)
+open import Relation.Nullary.Negation.Core using (contradiction)
+
 open ≤-Reasoning
 
 ------------------------------------------------------------------------
@@ -94,6 +100,15 @@ div-neg-is-neg-/ℕ n (ℕ.suc d) = -1*i≡-i (n /ℕ ℕ.suc d)
   rewrite div-pos-is-/ℕ n d {{d≢0}}
         = 0≤n⇒0≤n/ℕd n d 0≤n
 
+n<0⇒n/ℕd<0 : ∀ n d .{{_ : ℕ.NonZero d}} → n < 0ℤ → (n /ℕ d) < 0ℤ
+n<0⇒n/ℕd<0 -[1+ n ] d -<+
+  with ℕ.suc n ℕ.% d in sn%d
+... | ℕ.zero  = begin-strict
+  - (+ (ℕ.suc n ℕ./ d))   ≡⟨ cong (-_ ∘′ +_) (ℕ.sn%d≡0⇒sn/d≡s[n/d] n d sn%d) ⟩
+  - (+ (ℕ.suc (n ℕ./ d))) <⟨ -<+ ⟩
+  + 0                     ∎
+... | ℕ.suc _ = -<+
+
 [n/d]*d≤n : ∀ n d .{{_ : NonZero d}} → (n / d) * d ≤ n
 [n/d]*d≤n n (+ d) = begin
   n / + d * + d        ≡⟨ cong (_* (+ d)) (div-pos-is-/ℕ n d) ⟩
@@ -129,6 +144,175 @@ a≡a%n+[a/n]*n n d@(-[1+ _ ]) = begin-equality
   + r + - q * d      ≡⟨ cong (_+_ (+ r) ∘′ (_* d)) (sym (-1*i≡-i q)) ⟩
   + r + n / d * d    ∎
 
+0/ℕd≡0 : ∀ d .{{_ : ℕ.NonZero d}} → + 0 /ℕ d ≡ + 0
+0/ℕd≡0 d = cong (+_) (ℕ.0/n≡0 d)
+
+0/d≡0 : ∀ d .{{_ : NonZero d}} → + 0 / d ≡ + 0
+0/d≡0 (+ d) = trans (div-pos-is-/ℕ (+ 0) d) (0/ℕd≡0 d)
+0/d≡0 -[1+ d ] = trans (div-neg-is-neg-/ℕ (+ 0) (ℕ.suc d))
+                       (cong (-_) (0/ℕd≡0 (ℕ.suc d)))
+
+n/ℕ1≡n : ∀ n → n /ℕ 1 ≡ n
+n/ℕ1≡n (+ n) = cong +_ (ℕ.n/1≡n n)
+n/ℕ1≡n -[1+ n ] rewrite ℕ.n%1≡0 (ℕ.suc n) = cong (-_ ∘′ +_) (ℕ.n/1≡n (ℕ.suc n))
+
+n/1≡n : ∀ n → n / + 1 ≡ n
+n/1≡n n = trans (div-pos-is-/ℕ n 1) (n/ℕ1≡n n)
+
+n/ℕd≡0⇒∣n∣<d : ∀ n d .{{_ : ℕ.NonZero d}} → n /ℕ d ≡ 0ℤ → ∣ n ∣ ℕ.< d
+n/ℕd≡0⇒∣n∣<d (+ n) d _ with ℕ.zero ← n ℕ./ d in n/d≡0 = ℕ.m/n≡0⇒m<n n/d≡0
+n/ℕd≡0⇒∣n∣<d (-[1+ n ]) d n/ℕd≡0 with ℕ.zero ← ℕ.suc n ℕ.% d
+    | ℕ.suc n ℕ./ d in n/d
+... | ℕ.zero  = ℕ.m/n≡0⇒m<n n/d
+... | ℕ.suc _ = contradiction n/ℕd≡0 λ ()
+
+0≤n<d⇒n/ℕd≡0 : ∀ n d .{{_ : NonNegative n }} .{{_ : ℕ.NonZero d}} →
+                n < + d → n /ℕ d ≡ 0ℤ
+0≤n<d⇒n/ℕd≡0 (+ n) d (+<+ n<d) = cong (+_) (ℕ.m<n⇒m/n≡0 n<d)
+
+n/d≡0⇒∣n∣<∣d∣ : ∀ n d .{{_ : NonZero d}} → n / d ≡ 0ℤ → ∣ n ∣ ℕ.< ∣ d ∣
+n/d≡0⇒∣n∣<∣d∣ n (+ d) n/d≡0ℤ =
+              n/ℕd≡0⇒∣n∣<d n d (trans (sym (div-pos-is-/ℕ n d)) n/d≡0ℤ)
+n/d≡0⇒∣n∣<∣d∣ n -[1+ d ] n/d≡0ℤ =
+              n/ℕd≡0⇒∣n∣<d n (ℕ.suc d) (neg-injective {_} {+ 0}
+                (trans (sym (div-neg-is-neg-/ℕ n (ℕ.suc d))) n/d≡0ℤ))
+
+0≤n<∣d∣⇒n/d≡0 : ∀ n d .{{_ : NonNegative n }} .{{_ : NonZero d}} →
+                n < + ∣ d ∣ → n / d ≡ 0ℤ
+0≤n<∣d∣⇒n/d≡0 n (+ d) (+<+ n<d) = begin-equality
+  n / + d ≡⟨ div-pos-is-/ℕ n d ⟩
+  n /ℕ d  ≡⟨ (0≤n<d⇒n/ℕd≡0 n d (+<+ n<d)) ⟩
+  0ℤ ∎
+0≤n<∣d∣⇒n/d≡0 n -[1+ d ] (+<+ n<d) = begin-equality
+  n / -[1+ d ]     ≡⟨ div-neg-is-neg-/ℕ n (ℕ.suc d) ⟩
+  - (n /ℕ ℕ.suc d) ≡⟨ cong (-_) (0≤n<d⇒n/ℕd≡0 n (ℕ.suc d) (+<+ n<d)) ⟩
+  - 0ℤ ∎
+
+private
+  /ℕ-monoˡ-≤-pos-pos : ∀ n m d .{{_ : NonNegative n}} .{{_ : NonNegative m}}
+                       .{{_ : ℕ.NonZero d}} → n ≤ m → n /ℕ d ≤ m /ℕ d
+  /ℕ-monoˡ-≤-pos-pos _ _ d (+≤+ n≤m) = +≤+ (ℕ./-monoˡ-≤ d n≤m)
+
+  /ℕ-monoˡ-≤-neg-pos : ∀ n m d .{{_ : Negative n}} .{{_ : NonNegative m}}
+                       .{{_ : ℕ.NonZero d}} → n ≤ m → n /ℕ d ≤ m /ℕ d
+  /ℕ-monoˡ-≤-neg-pos n@(-[1+ _ ]) m@(+ _) d -≤+ =
+    <⇒≤ (<-≤-trans (n<0⇒n/ℕd<0 n d -<+) (0≤n⇒0≤n/ℕd m d (+≤+ z≤n)))
+
+  n≡sk>0 : ∀ {n k} → n ≡ ℕ.suc k → 0 ℕ.< n
+  n≡sk>0 n≡sk = ℕ.m<n⇒0<n (ℕ.≤-reflexive (sym n≡sk))
+
+  /ℕ-monoˡ-≤-neg-neg : ∀ n m d .{{_ : Negative n}} .{{_ : Negative m}}
+                       .{{_ : ℕ.NonZero d}} → n ≤ m → n /ℕ d ≤ m /ℕ d
+  /ℕ-monoˡ-≤-neg-neg (-[1+ n ]) (-[1+ m ]) d (-≤- m≤n)
+    with ℕ.suc n ℕ.% d in sn%d | ℕ.suc m ℕ.% d in sm%d
+  ... | ℕ.zero | ℕ.zero  = neg-mono-≤ (+≤+ (ℕ./-monoˡ-≤ d (s≤s m≤n)))
+  ... | ℕ.zero | ℕ.suc _ = let sm%d>0 = n≡sk>0 sm%d in begin
+    -(+(ℕ.suc n ℕ./ d))   ≡⟨ cong (-_ ∘′ +_) (ℕ.sn%d≡0⇒sn/d≡s[n/d] n d sn%d) ⟩
+    -[1+ n ℕ./ d ]        ≤⟨ -≤- (ℕ./-monoˡ-≤ d m≤n) ⟩
+    -[1+ m ℕ./ d ]        ≡⟨ cong -[1+_] (ℕ.sn%d>0⇒sn/d≡n/d m d sm%d>0)⟨
+    -[1+ ℕ.suc m ℕ./ d ]  ∎
+  ... | ℕ.suc _ | ℕ.zero  = let sn%d>0 = n≡sk>0 sn%d in begin
+    -[1+ ℕ.suc n ℕ./ d ]  ≡⟨ cong -[1+_] (ℕ.sn%d>0⇒sn/d≡n/d n d sn%d>0)⟩
+    -[1+ n ℕ./ d ]        ≤⟨ -≤- (ℕ./-monoˡ-≤ d m≤n) ⟩
+    -(+(ℕ.suc (m ℕ./ d))) ≡⟨ cong (-_ ∘′ +_) (ℕ.sn%d≡0⇒sn/d≡s[n/d] m d sm%d) ⟨
+    -(+(ℕ.suc m ℕ./ d))   ∎
+  ... | ℕ.suc _ | ℕ.suc _ = -≤- (ℕ./-monoˡ-≤ d (s≤s m≤n))
+
+/ℕ-monoˡ-≤ : ∀ d .{{_ : ℕ.NonZero d}} → Monotonic₁ _≤_ _≤_ (_/ℕ d)
+/ℕ-monoˡ-≤ d {n@(+ _)}      {m@(+ _)}      n≤m = /ℕ-monoˡ-≤-pos-pos n m d n≤m
+/ℕ-monoˡ-≤ d {n@(-[1+ _ ])} {m@(+ _)}      n≤m = /ℕ-monoˡ-≤-neg-pos n m d n≤m
+/ℕ-monoˡ-≤ d {n@(-[1+ _ ])} {m@(-[1+ _ ])} n≤m = /ℕ-monoˡ-≤-neg-neg n m d n≤m
+
+/ℕ-monoʳ-≤-nonNeg : ∀ n {d₁ d₂} .{{_ : ℕ.NonZero d₁}} .{{_ : ℕ.NonZero d₂}}
+                    .{{_ : NonNegative n}} → d₁ ℕ.≤ d₂ → n /ℕ d₂ ≤ n /ℕ d₁
+/ℕ-monoʳ-≤-nonNeg (+ n) {d₁} {d₂} d₁≤d₂ = +≤+ (ℕ./-monoʳ-≤ n d₁≤d₂)
+
+/ℕ-monoʳ-≤-nonPos : ∀ n {d₁ d₂} .{{_ : ℕ.NonZero d₁}} .{{_ : ℕ.NonZero d₂}}
+                    .{{_ : NonPositive n}} → d₁ ℕ.≤ d₂ → n /ℕ d₁ ≤ n /ℕ d₂
+/ℕ-monoʳ-≤-nonPos (+ 0) {d₁} {d₂} d₁≤d₂ =
+  ≤-trans (≤-reflexive (0/ℕd≡0 d₁)) (≤-reflexive (sym (0/ℕd≡0 d₂)))
+/ℕ-monoʳ-≤-nonPos -[1+ n ] {d₁} {d₂} d₁≤d₂
+  with ℕ.suc n ℕ.% d₁ in sn%d₁ | ℕ.suc n ℕ.% d₂ in sn%d₂
+... | ℕ.zero | ℕ.zero  = neg-mono-≤ (+≤+ (ℕ./-monoʳ-≤ (ℕ.suc n) d₁≤d₂))
+... | ℕ.zero | ℕ.suc _ = let sn%d₂>0 = n≡sk>0 sn%d₂ in begin
+  -(+ (ℕ.suc n ℕ./ d₁)) ≡⟨ cong (-_ ∘′ +_) (ℕ.sn%d≡0⇒sn/d≡s[n/d] n d₁ sn%d₁) ⟩
+  -[1+ n ℕ./ d₁ ]       ≤⟨ -≤- (ℕ./-monoʳ-≤ n d₁≤d₂) ⟩
+  -[1+ n ℕ./ d₂ ]       ≡⟨ cong -[1+_] (ℕ.sn%d>0⇒sn/d≡n/d n d₂ sn%d₂>0) ⟨
+  -[1+ ℕ.suc n ℕ./ d₂ ] ∎
+... | ℕ.suc _ | ℕ.zero  = let sn%d₁>0 = n≡sk>0 sn%d₁ in begin
+  -[1+ ℕ.suc n ℕ./ d₁ ]   ≡⟨ cong -[1+_] (ℕ.sn%d>0⇒sn/d≡n/d n d₁ sn%d₁>0) ⟩
+  -[1+ n ℕ./ d₁ ]         ≤⟨ -≤- (ℕ./-monoʳ-≤ n d₁≤d₂) ⟩
+  -(+ (ℕ.suc (n ℕ./ d₂))) ≡⟨ cong (-_ ∘′ +_) (ℕ.sn%d≡0⇒sn/d≡s[n/d] n d₂ sn%d₂)⟨
+  -(+ (ℕ.suc n ℕ./ d₂))   ∎
+... | ℕ.suc _ | ℕ.suc _ = -≤- (ℕ./-monoʳ-≤ (ℕ.suc n) d₁≤d₂)
+
+/-monoˡ-≤-pos : ∀ d .{{_ : NonZero d}} .{{_ : Positive d}} →
+                Monotonic₁ _≤_ _≤_ (_/ d)
+/-monoˡ-≤-pos (+ d) {n} {m} n≤m = begin
+  n / (+ d) ≡⟨ div-pos-is-/ℕ n d ⟩
+  n /ℕ d    ≤⟨ /ℕ-monoˡ-≤ d n≤m ⟩
+  m /ℕ d    ≡⟨ div-pos-is-/ℕ m d ⟨
+  m / + d   ∎
+
+/-monoˡ-≤-neg : ∀ d .{{_ : NonZero d}} .{{_ : Negative d}} →
+                Monotonic₁ _≤_ _≥_ (_/ d)
+/-monoˡ-≤-neg -[1+ d ] {n} {m} n≤m = begin
+  m / -[1+ d ]     ≡⟨ div-neg-is-neg-/ℕ m (ℕ.suc d) ⟩
+  - (m /ℕ ℕ.suc d) ≤⟨ neg-mono-≤ (/ℕ-monoˡ-≤ (ℕ.suc d) n≤m) ⟩
+  - (n /ℕ ℕ.suc d) ≡⟨ div-neg-is-neg-/ℕ n (ℕ.suc d) ⟨
+  n / - +[1+ d ]   ∎
+
+/-monoʳ-≤-nonNeg-eq-signs : ∀ n {d₁ d₂} .{{_ : NonZero d₁}} .{{_ : NonZero d₂}}
+                            .{{_ : NonNegative n}} → {sign d₁ ≡ sign d₂} →
+                            d₁ ≤ d₂ → n / d₁ ≥ n / d₂
+/-monoʳ-≤-nonNeg-eq-signs n {+ d₁} {+ d₂} (+≤+ d₁≤d₂) = begin
+  n / + d₂ ≡⟨ div-pos-is-/ℕ n d₂ ⟩
+  n /ℕ d₂  ≤⟨ /ℕ-monoʳ-≤-nonNeg n d₁≤d₂ ⟩
+  n /ℕ d₁  ≡⟨ div-pos-is-/ℕ n d₁ ⟨
+  n / + d₁ ∎
+/-monoʳ-≤-nonNeg-eq-signs n { -[1+ d₁ ] } { -[1+ d₂ ] } (-≤- d₂≤d₁) = begin
+  n / -[1+ d₂ ]     ≡⟨ div-neg-is-neg-/ℕ n (ℕ.suc d₂) ⟩
+  - (n /ℕ ℕ.suc d₂) ≤⟨ neg-mono-≤ (/ℕ-monoʳ-≤-nonNeg n (s≤s d₂≤d₁)) ⟩
+  - (n /ℕ ℕ.suc d₁) ≡⟨ div-neg-is-neg-/ℕ n (ℕ.suc d₁) ⟨
+  n / - +[1+ d₁ ]   ∎
+
+/-monoʳ-≤-nonPos-eq-signs : ∀ n {d₁ d₂} .{{_ : NonZero d₁}} .{{_ : NonZero d₂}}
+                            .{{_ : NonPositive n}} → {sign d₁ ≡ sign d₂} →
+                            d₁ ≤ d₂ → n / d₁ ≤ n / d₂
+/-monoʳ-≤-nonPos-eq-signs n {+ d₁} {+ d₂} (+≤+ d₁≤d₂) = begin
+  n / + d₁ ≡⟨ div-pos-is-/ℕ n d₁ ⟩
+  n /ℕ d₁  ≤⟨ /ℕ-monoʳ-≤-nonPos n d₁≤d₂ ⟩
+  n /ℕ d₂  ≡⟨ div-pos-is-/ℕ n d₂ ⟨
+  n / + d₂ ∎
+/-monoʳ-≤-nonPos-eq-signs n { -[1+ d₁ ] } { -[1+ d₂ ] } (-≤- d₂≤d₁) = begin
+  n / -[1+ d₁ ]     ≡⟨ div-neg-is-neg-/ℕ n (ℕ.suc d₁) ⟩
+  - (n /ℕ ℕ.suc d₁) ≤⟨ neg-mono-≤ (/ℕ-monoʳ-≤-nonPos n (s≤s d₂≤d₁)) ⟩
+  - (n /ℕ ℕ.suc d₂) ≡⟨ div-neg-is-neg-/ℕ n (ℕ.suc d₂) ⟨
+  n / - +[1+ d₂ ]   ∎
+
+/-monoʳ-≤-nonNeg-op-signs : ∀ n {d₁ d₂} .{{_ : NonZero d₁}} .{{_ : NonZero d₂}}
+                            .{{_ : NonNegative n}} →
+                            {sign d₁ ≡ opposite (sign d₂)} →
+                            d₁ ≤ d₂ → n / d₁ ≤ n / d₂
+/-monoʳ-≤-nonNeg-op-signs n { -[1+ d₁ ]} {+ d₂} -≤+ = begin
+  n / -[1+ d₁ ]     ≡⟨ div-neg-is-neg-/ℕ n (ℕ.suc d₁) ⟩
+  - (n /ℕ ℕ.suc d₁) ≤⟨ neg-mono-≤ (0≤n⇒0≤n/ℕd n (ℕ.suc d₁) (nonNegative⁻¹ n)) ⟩
+  0ℤ                ≤⟨ 0≤n⇒0≤n/d n (+ d₂) (nonNegative⁻¹ n) (+≤+ z≤n) ⟩
+  n / + d₂          ∎
+
+/-monoʳ-≤-nonPos-op-signs : ∀ n {d₁ d₂} .{{_ : NonZero d₁}} .{{_ : NonZero d₂}}
+                           .{{_ : NonPositive n}} →
+                           {sign d₁ ≡ opposite (sign d₂)} →
+                           d₁ ≤ d₂ → n / d₁ ≥ n / d₂
+/-monoʳ-≤-nonPos-op-signs (+ 0) {d₁@(-[1+ _ ])} {d₂@(+ _)} -≤+ =
+   ≤-trans (≤-reflexive (0/d≡0 d₂)) (≤-reflexive (sym (0/d≡0 d₁)))
+/-monoʳ-≤-nonPos-op-signs n@(-[1+ _ ]) { -[1+ d₁ ]} {+ d₂} -≤+ = begin
+  n / + d₂          ≡⟨ div-pos-is-/ℕ n d₂ ⟩
+  n /ℕ d₂           <⟨ n<0⇒n/ℕd<0 n d₂ (negative⁻¹ n) ⟩
+  0ℤ                <⟨ neg-mono-< (n<0⇒n/ℕd<0 n (ℕ.suc d₁) (negative⁻¹ n)) ⟩
+  - (n /ℕ ℕ.suc d₁) ≡⟨ div-neg-is-neg-/ℕ n (ℕ.suc d₁) ⟨
+  n / -[1+ d₁ ]     ∎
+
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
 ------------------------------------------------------------------------
diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda
index 86bc8d3168..044623c611 100644
--- a/src/Data/Nat/DivMod.agda
+++ b/src/Data/Nat/DivMod.agda
@@ -121,6 +121,13 @@ 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-
 [1+m%d]≤1+n⇒[m%d]≤n : ∀ m n d .{{_ : NonZero d}} → 0 < suc m % d → suc m % d ≤ suc n → m % d ≤ n
 [1+m%d]≤1+n⇒[m%d]≤n m n (suc d-1) leq = 1+a[modₕ]n≤1+k⇒a[modₕ]n≤k 0 n m d-1 leq
 
+%-pred-≡suc : ∀ m d k .{{_ : NonZero d}} → suc m % d ≡ suc k → m % d ≡ k
+%-pred-≡suc m d k sm%d≡sk = ≤-antisym m%d≤k k≤m%d
+  where
+  k<sm%d = ≤-reflexive (sym sm%d≡sk)
+  m%d≤k = ([1+m%d]≤1+n⇒[m%d]≤n m k d (m<n⇒0<n k<sm%d) (≤-reflexive sm%d≡sk))
+  k≤m%d = m<[1+n%d]⇒m≤[n%d] m d k<sm%d
+
 %-distribˡ-+ : ∀ m n d .{{_ : NonZero d}} → (m + n) % d ≡ ((m % d) + (n % d)) % d
 %-distribˡ-+ m n d@(suc d-1) = begin-equality
   (m + n)                         % d ≡⟨ cong (λ v → (v + n) % d) (m≡m%n+[m/n]*n m d) ⟩
@@ -292,6 +299,43 @@ m/n≡1+[m∸n]/n {m@(suc m-1)} {n@(suc n-1)} m≥n = begin-equality
   pred (1 + (m ∸ n) / n) ≡⟨ cong pred (m/n≡1+[m∸n]/n n≥m) ⟨
   pred (m / n)           ∎
 
+sn%d≡0⇒sn/d≡s[n/d] : ∀ n d .{{_ : NonZero d}} → suc n % d ≡ 0 →
+                     suc n / d ≡ suc (n / d)
+sn%d≡0⇒sn/d≡s[n/d] n d@(suc _) sn%d≡0 =
+  *-cancelʳ-≡ (suc n / d) (suc (n / d)) d (begin-equality
+    suc n / d * d           ≡⟨ sn≡[sn/d]*d ⟨
+    suc n                   ≡⟨ cong suc (m≡m%n+[m/n]*n n d) ⟩
+    suc (n % d) + n / d * d ≡⟨ cong (_+ n / d * d) s[n%d]≡d ⟩
+    d + n / d * d           ≡⟨ cong (_+ n / d * d) (*-identityˡ d) ⟨
+    1 * d + n / d * d       ≡⟨ *-distribʳ-+ d 1 (n / d) ⟨
+    (1 + n / d) * d ∎ )
+  where
+  sn≡[sn/d]*d = trans (m≡m%n+[m/n]*n (suc n) d)
+                      (cong (_+ suc n / d * d) sn%d≡0)
+  s[n%d]≡d = trans (cong suc (%-pred-≡0 sn%d≡0)) (∸-suc z≤n)
+
+sn%d>0⇒sn/d≡n/d : ∀ n d .{{_ : NonZero d}} →
+                  0 < suc n % d → suc n / d ≡ n / d
+sn%d>0⇒sn/d≡n/d n d 0<sn%d with suc k ← suc n % d in sn%d≡sk =
+  *-cancelʳ-≡ (suc n / d) (n / d) d (begin-equality
+    suc n / d * d
+      ≡⟨ [n/d]*d≡n∸n%d (suc n) d ⟩
+    suc n ∸ suc n % d
+      ≡⟨ cong (suc n ∸_) sn%d≡sk ⟩
+    suc n ∸ suc k
+      ≡⟨ cong (λ x → suc x ∸ suc k) (m≡m%n+[m/n]*n n d) ⟩
+    suc (n % d) + n / d * d ∸ suc k
+      ≡⟨ cong (λ x → suc x + n / d * d ∸ suc k) (%-pred-≡suc n d k sn%d≡sk) ⟩
+    suc k + n / d * d ∸ suc k
+      ≡⟨ m+n∸m≡n (suc k) (n / d * d) ⟩
+    n / d * d ∎)
+  where
+  [n/d]*d≡n∸n%d : ∀ n d .{{_ : NonZero d}} → (n / d) * d ≡ n ∸ n % d
+  [n/d]*d≡n∸n%d n d = sym (begin-equality
+    n ∸ n % d           ≡⟨ cong (n ∸_) (m%n≡m∸m/n*n n d) ⟩
+    n ∸ (n ∸ n / d * d) ≡⟨ m∸[m∸n]≡n (m/n*n≤m n d) ⟩
+    n / d * d           ∎)
+
 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
@@ -492,4 +536,3 @@ m divMod n = result (m / n) (m mod n) $ begin-equality
   m % n                + [m/n]*n  ≡⟨ cong (_+ [m/n]*n) (toℕ-fromℕ< [m%n]<n) ⟨
   toℕ (fromℕ< [m%n]<n) + [m/n]*n  ∎
   where [m/n]*n = m / n * n ; [m%n]<n = m%n<n m n
-
diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda
index 24fe04681a..8705d10733 100644
--- a/src/Data/Rational/Unnormalised/Properties.agda
+++ b/src/Data/Rational/Unnormalised/Properties.agda
@@ -31,10 +31,11 @@ open import Data.Bool.Base using (T; true; false)
 open import Data.Nat.Base as ℕ using (suc; pred)
 import Data.Nat.Properties as ℕ
   using (≤-refl; +-comm; +-identityʳ; +-assoc
-        ; *-identityʳ; *-comm; *-assoc; *-suc)
+        ; *-identityˡ; *-identityʳ; *-comm; *-assoc; *-suc; m*n≢0)
 open import Data.Integer.Base as ℤ using (ℤ; +0; +[1+_]; -[1+_]; 0ℤ; 1ℤ; -1ℤ)
 open import Data.Integer.Solver renaming (module +-*-Solver to ℤ-solver)
 import Data.Integer.Properties as ℤ
+import Data.Integer.DivMod as ℤ
 open import Data.Rational.Unnormalised.Base
 open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Data.Sum.Base as Sum using (_⊎_; [_,_]′; inj₁; inj₂)
@@ -89,6 +90,9 @@ private
 ↧[n/d]≡d : ∀ n d .{{_ : ℕ.NonZero d}} → ↧ (n / d) ≡ ℤ.+ d
 ↧[n/d]≡d n (suc d) = refl
 
+↧ₙ[n/d]≡d : ∀ n d .{{_ : ℕ.NonZero d}} → ↧ₙ (n / d) ≡ d
+↧ₙ[n/d]≡d n (suc d) = refl
+
 ------------------------------------------------------------------------
 -- Properties of _≃_
 ------------------------------------------------------------------------
@@ -1565,6 +1569,94 @@ p>1⇒1/p<1 {p} p>1 = lemma′ p (p>1⇒p≢0 p>1) p>1
     1/q≥0 : NonNegative 1/q
     1/q≥0 = pos⇒nonNeg 1/q {{1/pos⇒pos q}}
 
+------------------------------------------------------------------------
+-- Properties of _/_
+
+n/d≡[n/1]*[1/d] : ∀ n d .{{_ : ℕ.NonZero d}} → n / d ≡ (n / 1) * (1ℤ / d)
+n/d≡[n/1]*[1/d] n d@(suc _) = sym (/-cong (ℤ.*-identityʳ n) (ℕ.*-identityˡ d))
+
+n/d≃[n/a]*[a/d] : ∀ n d a .{{_ : ℕ.NonZero d}} .{{_ : ℕ.NonZero a}} →
+                  n / d ≃ (n / a) * (ℤ.+ a / d)
+n/d≃[n/a]*[a/d] n d a = let +a = ℤ.+ a in ≃-sym (begin-equality
+  n / a * (+a / d)
+        ≡⟨ *-eta (n / a) (+a / d) ⟩
+  (↥ (n / a) ℤ.* ↥ (+a / d)) / (↧ₙ (n / a) ℕ.* ↧ₙ (+a / d))
+        ≡⟨ /-cong {{_}} {{a*d≢0}}
+                  (cong₂ ℤ._*_ (↥[n/d]≡n n a) (↥[n/d]≡n +a d))
+                  (cong₂ ℕ._*_ (↧ₙ[n/d]≡d n a) (↧ₙ[n/d]≡d +a d)) ⟩
+  ((n ℤ.* +a) / (a ℕ.* d)) {{a*d≢0}}
+        ≡⟨ /-cong {{_}} {{a*d≢0}} (ℤ.*-comm n +a) refl ⟩
+  ((+a ℤ.* n) / (a ℕ.* d)) {{a*d≢0}}
+        ≃⟨ *-cancelˡ-/ a {{_}} {{a*d≢0}} ⟩
+  n / d ∎)
+  where
+  open ≤-Reasoning
+  *-eta : ∀ p q → p * q ≡ (↥ p ℤ.* ↥ q) / (↧ₙ p ℕ.* ↧ₙ q)
+  *-eta p@record{} q@record{} = refl
+  a*d≢0 : ℕ.NonZero (a ℕ.* d)
+  a*d≢0 = ℕ.m*n≢0 a d
+
+------------------------------------------------------------------------
+-- Properties of _/_ and _+_
+
+private
+  [n+m]/1≡n/1+m/1 : ∀ n m → (n ℤ.+ m) / 1 ≡ n / 1 + m / 1
+  [n+m]/1≡n/1+m/1 n m = sym (begin
+    (n ℤ.* 1ℤ ℤ.+ m ℤ.* 1ℤ) / (1 ℕ.* 1)
+       ≡⟨ /-cong (cong₂ ℤ._+_ (ℤ.*-identityʳ n) (ℤ.*-identityʳ m))
+                (ℕ.*-identityʳ 1) ⟩
+    (n ℤ.+ m) / 1 ∎)
+    where open ≡-Reasoning
+
+/-distribʳ-+ : ∀ d n m .{{_ : ℕ.NonZero d}} → (n ℤ.+ m) / d ≃ n / d + m / d
+/-distribʳ-+ d n m = begin
+  (n ℤ.+ m) / d
+      ≡⟨ n/d≡[n/1]*[1/d] (n ℤ.+ m) d ⟩
+  (n ℤ.+ m) / 1 * (1ℤ / d)
+      ≡⟨ cong (_* (1ℤ / d)) ([n+m]/1≡n/1+m/1 n m) ⟩
+  (n / 1 + m / 1) * (1ℤ / d)
+      ≈⟨ *-distribʳ-+ (1ℤ / d) (n / 1) (m / 1) ⟩
+  n / 1 * (1ℤ / d) + m / 1 * (1ℤ / d)
+      ≡⟨ cong₂ _+_ (n/d≡[n/1]*[1/d] n d) (n/d≡[n/1]*[1/d] m d) ⟨
+  n / d + m / d ∎
+  where open ≃-Reasoning
+
+------------------------------------------------------------------------
+-- Properties of _/_ and _<_
+
+/-monoˡ-< : ∀ d .{{_ : ℕ.NonZero d}} → Monotonic₁ ℤ._<_ _<_ (_/ d)
+/-monoˡ-< d@(suc _) n<m = *<* (ℤ.*-monoʳ-<-pos (ℤ.+ d) n<m)
+
+/-monoʳ-<-pos : ∀ n {d₁ d₂} .{{_ : ℤ.Positive n}}
+                .{{_ : ℕ.NonZero d₁}} .{{_ : ℕ.NonZero d₂}} →
+                d₁ ℕ.< d₂ → n / d₂ < n / d₁
+/-monoʳ-<-pos n {d₁@(suc _)} {d₂@(suc _)} d₁<d₂ =
+              *<* (ℤ.*-monoˡ-<-pos n (ℤ.+<+ d₁<d₂))
+
+/-monoʳ-<-neg : ∀ n {d₁ d₂} .{{_ : ℤ.Negative n}}
+                .{{_ : ℕ.NonZero d₁}} .{{_ : ℕ.NonZero d₂}} →
+                d₁ ℕ.< d₂ → n / d₁ < n / d₂
+/-monoʳ-<-neg n {d₁@(suc _)} {d₂@(suc _)} d₁<d₂ =
+              *<* (ℤ.*-monoˡ-<-neg n (ℤ.+<+ d₁<d₂))
+
+------------------------------------------------------------------------
+-- Properties of _/_ and _≤_
+
+/-monoˡ-≤ : ∀ d .{{_ : ℕ.NonZero d}} → Monotonic₁ ℤ._≤_ _≤_ (_/ d)
+/-monoˡ-≤ d@(suc _) n≤m = *≤* (ℤ.*-monoʳ-≤-nonNeg (ℤ.+ d) n≤m)
+
+/-monoʳ-≤-nonNeg : ∀ n {d₁ d₂} .{{_ : ℤ.NonNegative n}}
+                   .{{_ : ℕ.NonZero d₁}} .{{_ : ℕ.NonZero d₂}} →
+                   d₁ ℕ.≤ d₂ → n / d₂ ≤ n / d₁
+/-monoʳ-≤-nonNeg n {d₁@(suc _)} {d₂@(suc _)} d₁≤d₂ =
+                 *≤* (ℤ.*-monoˡ-≤-nonNeg n (ℤ.+≤+ d₁≤d₂))
+
+/-monoʳ-≤-nonPos : ∀ n {d₁ d₂} .{{_ : ℤ.NonPositive n}}
+                   .{{_ : ℕ.NonZero d₁}} .{{_ : ℕ.NonZero d₂}} →
+                   d₁ ℕ.≤ d₂ → n / d₁ ≤ n / d₂
+/-monoʳ-≤-nonPos n {d₁@(suc _)} {d₂@(suc _)} d₁≤d₂ =
+                 *≤* (ℤ.*-monoˡ-≤-nonPos n (ℤ.+≤+ d₁≤d₂))
+
 ------------------------------------------------------------------------
 -- Properties of _⊓_ and _⊔_
 ------------------------------------------------------------------------
@@ -1933,7 +2025,6 @@ pos⊔pos⇒pos p q = positive (⊔-mono-< (positive⁻¹ p) (positive⁻¹ q))
 ∣-∣-nonNeg (mkℚᵘ +0       _) = _
 ∣-∣-nonNeg (mkℚᵘ -[1+ _ ] _) = _
 
-
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
 ------------------------------------------------------------------------