diff --git a/CHANGELOG.md b/CHANGELOG.md
index efab9e7df7..47d0a49c0c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -396,6 +396,14 @@ Additions to existing modules
   viaList : (List A → List B) → (DiffList A → DiffList B)
   ```
 
+* In `Data.Bool.Properties`:
+  ```agda
+  T-to-≡     : ∀ {x} → T x       → x ≡ true
+  ≡-to-T     : ∀ {x} → x ≡ true  → T x
+  T-not-to-≡ : ∀ {x} → T (not x) → x ≡ false
+  ≡-to-T-not : ∀ {x} → x ≡ false → T (not x)
+  ```
+
 * In `Data.DifferenceList.Properties`:
   ```agda
   fromList-++ : ∀ xs ys → fromList (xs List.++ ys) ≗ fromList xs ++ fromList ys
@@ -404,9 +412,55 @@ Additions to existing modules
   viaList⁺ : (f : List A → List B) → xs ∼ dxs → f xs ∼ viaList f dxs
   ```
 
+* In `Data.Integer.Base`:
+  ```
+  _<ᵇ_ : ℤ → ℤ → Bool
+  -≤-⁻¹ : ∀ {m} {n} → -[1+ m ] ≤ -[1+ n ] → n ℕ.≤ m
+  +≤+⁻¹ : ∀ {m} {n} → + m      ≤ + n      → m ℕ.≤ n
+  -<-⁻¹ : ∀ {m} {n} → -[1+ m ] < -[1+ n ] → n ℕ.< m
+  +<+⁻¹ : ∀ {m} {n} → + m      < + n      → m ℕ.< n
+  ```
+
+* In `Data.Integer.DivMod`:
+  ```agda
+  i/ℕ1≡i : ∀ i → i /ℕ 1 ≡ i
+  i/1≡i : ∀ i → i / + 1 ≡ i
+  /ℕ-congʳ : ∀ i {m} {n} .{{_ : ℕ.NonZero m}} → .{{_ : ℕ.NonZero n}} →
+             m ≡ n → i /ℕ m ≡ i /ℕ n
+  nonNeg[i]⇒i/ℕd      : ∀ i d .{{_ : ℕ.NonZero d}} .{{_ : NonNegative i}} →
+                        i /ℕ d ≡ + (∣ i ∣ ℕ./ d)
+  neg[i]∧∣i∣%d≡0⇒i/ℕd : ∀ i {d} .{{_ : ℕ.NonZero d}} .{{_ : Negative i}} →
+                        ∣ i ∣ ℕ.% d ≡ 0 → i /ℕ d ≡ - (+ (∣ i ∣ ℕ./ d))
+  neg[i]∧∣i∣%d≢0⇒i/ℕd : ∀ i d .{{_ : ℕ.NonZero d}} .{{_ : Negative i}}
+                        .{{_ : ℕ.NonZero (∣ i ∣ ℕ.% d)}} → i /ℕ d ≡ -[1+ ∣ i ∣ ℕ./ d ]
+  *-cancelˡ-/ℕ : ∀ m i n .{{_ : ℕ.NonZero n}} .{{_ : ℕ.NonZero (m ℕ.* n)}} →
+                 (+ m * i) /ℕ (m ℕ.* n) ≡ i /ℕ n
+  *-cancelʳ-/ℕ : ∀ i m n .{{_ : ℕ.NonZero n}} .{{_ : ℕ.NonZero (n ℕ.* m)}} →
+                 (i * + m) /ℕ (n ℕ.* m) ≡ i /ℕ n
+  *-cancelˡ-/ : ∀ i j k .{{_ : NonZero k}} .{{_ : NonZero (i * k)}} →
+                .{{_ : NonNegative i}} → (i * j) / (i * k) ≡ j / k
+  *-cancelʳ-/ : ∀ i j k .{{_ : NonZero k}} .{{_ : NonZero (k * j)}} →
+                .{{_ : NonNegative j}} → (i * j) / (k * j) ≡ i / k
+  ```
+
 * In `Data.Integer.GCD`:
   ```agda
-  gcd[i,i]≡∣i∣ : ∀ i → gcd i i ≡ + ∣i∣
+    gcd[i,i]≡∣i∣ : ∀ i → gcd i i ≡ + ∣i∣
+  ```
+
+* In `Data.Integer.Properties`:
+  ```
+  <ᵇ⇒< : T (i <ᵇ j) → i < j
+  <⇒<ᵇ : i < j → T (i <ᵇ j)
+  nonZero⁻¹          : ∀ i → .{{NonZero i}} → i ≢ 0ℤ
+  nonNeg∧nonZero⇒Pos : ∀ i → .{{NonNegative i}} → .{{NonZero i}} → Positive i
+  ∣i-j∣≡0⇒i≡j        : ∀ {i} {j} → ∣ i - j ∣ ≡ 0 → i ≡ j
+  i*j≢0⇒i≢0          : ∀ i {j} .{{_ : NonZero (i * j)}} → NonZero i
+  i*j≢0⇒j≢0          : ∀ i {j} .{{_ : NonZero (i * j)}} → NonZero j
+  i≥0∧j≥0⇒i*j≥0      : ∀ i j → .{{NonNegative i}} → .{{NonNegative j}} →
+                       NonNegative (i * j)
+  i>0∧j<0⇒i*j<0      : ∀ i j → .{{Positive i}} → .{{Negative j}} →
+                       Negative (i * j)
   ```
 
 * In `Data.List.Membership.Propositional.Properties`:
@@ -437,6 +491,8 @@ Additions to existing modules
 * In `Data.Nat.DivMod`:
   ```agda
   m<suc[m/n]*n : ∀ m n → m < suc (m / n) * n
+  m*n%o≡m*n%[m*o] : ∀ m n o .{{_ : NonZero o}} .{{_ : NonZero (m * o)}} →
+                    m * (n % o) ≡ (m * n) % (m * o)
   ```
 
 * In `Data.Nat.GCD`:
@@ -468,6 +524,7 @@ Additions to existing modules
   m≢0∧n≢0⇒m+n≢0 : ∀ m .{{_ : NonZero m}} n .{{_ : NonZero n}} → NonZero (m + n)
   m+n≢0⇒m≢0∨n≢0 : ∀ m n .{{_ : NonZero (m + n)} → NonZero m ⊎ NonZero n
   *-almostCancelʳ-≡ : AlmostRightCancellative 0 _*_
+  m*n≡0⇒n≡0 : ∀ m n .{{_ : NonZero m}} → m * n ≡ 0 → n ≡ 0
   ```
 
 * In `Data.Product`:
@@ -491,6 +548,42 @@ Additions to existing modules
                     i / n + j / n ≡ (i ℤ.+ j) / n
   ```
 
+* In `Data.Rational.Unnormalised.Properties`:
+  ```agda
+  ≤ᵇ-reflects-≤       : ∀ p q → Reflects (p ≤ q) (p ≤ᵇ q)
+  ≰ᵇ⇒≰                : T (not (p ≤ᵇ q)) → p ≰ q
+  ≰⇒≰ᵇ                : p ≰ q → T (not (p ≤ᵇ q))
+  <ᵇ-reflects-<       : ∀ p q → Reflects (p < q) (p <ᵇ q)
+  ≮ᵇ⇒≮                : T (not (p <ᵇ q)) → p ≮ q
+  ≮⇒≮ᵇ                : p ≮ q → T (not (p <ᵇ q))
+  neg-distrib-minus   : ∀ p q → - (p - q) ≡ q - p
+  /-cancelʳ-<         : ∀ {i} {j} d .{{_ : ℕ.NonZero d}} → i / d < j / d → i ℤ.< j
+  /-cancelʳ-≤         : ∀ {i} {j} d .{{_ : ℕ.NonZero d}} → i / d ≤ j / d → i ℤ.≤ j
+  ∣p-q∣≤∣p-r∣+∣r-q∣   : ∀ p q r → ∣ p - q ∣ ≤ ∣ p - r ∣ + ∣ r - q ∣
+  ∣p-q∣≡∣q-p∣         : ∀ p q → ∣ p - q ∣ ≡ ∣ q - p ∣
+  -q≤p≤q⇒|p|≤q        : - q ≤ p → p ≤ q → ∣ p ∣ ≤ q
+  -q<p<q⇒∣p∣<q        : ∀ {p q} → - q < p → p < q → ∣ p ∣ < q
+  floor-cong          : ∀ {p} {q} → p ≃ q → ⌊ p ⌋ ≡ ⌊ q ⌋
+  ceiling-cong        : ∀ {p} {q} → p ≃ q → ⌈ p ⌉ ≡ ⌈ q ⌉
+  round-cong          : ∀ {p} {q} → p ≃ q → round p ≡ round q
+  ⌊i/1⌋≡i             : ∀ i → ⌊ i / 1 ⌋ ≡ i
+  ⌈i/1⌉≡i             : ∀ i → ⌈ i / 1 ⌉ ≡ i
+  ⌊-q⌋≡-⌈q⌉           : ∀ q → ⌊ - q ⌋ ≡ ℤ.- ⌈ q ⌉
+  ⌈-q⌉≡-⌊q⌋           : ∀ q → ⌈ - q ⌉ ≡ ℤ.- ⌊ q ⌋
+  round[-q]≡-round[q] : ∀ q → round (- q) ≡ ℤ.- (round q)
+  ⌊q⌋≤q               : ⌊ q ⌋ / 1 ≤ q
+  q<⌊q⌋+1             : q < ⌊ q ⌋ / 1 + 1ℚᵘ
+  q≤⌈q⌉               : q ≤ ⌈ q ⌉ / 1
+  ⌈q⌉-1<q             : ⌈ q ⌉ / 1 - 1ℚᵘ < q
+  ⌈q⌉≤⌊q⌋+1           : ∀ q → ⌈ q ⌉ ℤ.≤ ⌊ q ⌋ ℤ.+ 1ℤ
+  ∣q-⌊q⌋∣<1           : ∀ q → ∣ q - ⌊ q ⌋ / 1 ∣ < 1ℚᵘ
+  ∣q-⌈q⌉∣<1           : ∀ q → ∣ q - ⌈ q ⌉ / 1 ∣ < 1ℚᵘ
+  ∣q-round[q]∣≤½      : ∀ q → ∣ q - (round q) / 1 ∣ ≤ ½
+  i≤q⇒i≤⌊q⌋           : ∀ i q → i / 1 ≤ q → i ℤ.≤ ⌊ q ⌋
+  q≤i⇒⌈q⌉≤i           : ∀ i q → q ≤ i / 1 → ⌈ q ⌉ ℤ.≤ i
+  ∣q-round[q]∣≤∣q-i∣  : ∀ q i → ∣ q - (round q) / 1 ∣ ≤ ∣ q - i / 1 ∣
+  ```
+
 * In `Data.Sum.Relation.Binary.Pointwise`:
   ```agda
   elim : R =[ f ]⇒ T → S =[ g ]⇒ T →
@@ -592,6 +685,14 @@ Additions to existing modules
   surjective : Surjective _≈₁_ _≈₂_ to
   ```
 
+* In `Relation.Nullary.Reflects`
+  ```agda
+  reflects-true   : ∀ {b} → Reflects A b → b ≡ true  → A
+  reflects-false  : ∀ {b} → Reflects A b → b ≡ false → ¬ A
+  reflects-proof  : ∀ {b} → Reflects A b → A         → b ≡ true
+  reflects-refute : ∀ {b} → Reflects A b → ¬ A       → b ≡ false
+  ```
+
 * In `Function.Structures.IsRightInverse`:
   ```agda
   injective   : Injective _≈₁_ _≈₂_ to
diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda
index ef51693834..e8abe2d70c 100644
--- a/src/Data/Bool/Properties.agda
+++ b/src/Data/Bool/Properties.agda
@@ -853,10 +853,22 @@ T-≡ : ∀ {x} → T x ⇔ x ≡ true
 T-≡ {false} = mk⇔ (λ ())       (λ ())
 T-≡ {true}  = mk⇔ (const refl) (const _)
 
+T-to-≡ : ∀ {x} → T x → x ≡ true
+T-to-≡ = Equivalence.to T-≡
+
+≡-to-T : ∀ {x} → x ≡ true → T x
+≡-to-T = Equivalence.from T-≡
+
 T-not-≡ : ∀ {x} → T (not x) ⇔ x ≡ false
 T-not-≡ {false} = mk⇔ (const refl) (const _)
 T-not-≡ {true}  = mk⇔ (λ ())       (λ ())
 
+T-not-to-≡ : ∀ {x} → T (not x) → x ≡ false
+T-not-to-≡ = Equivalence.to T-not-≡
+
+≡-to-T-not : ∀ {x} → x ≡ false → T (not x)
+≡-to-T-not = Equivalence.from T-not-≡
+
 T-∧ : ∀ {x y} → T (x ∧ y) ⇔ (T x × T y)
 T-∧ {true}  {true}  = mk⇔ (const (_ , _)) (const _)
 T-∧ {true}  {false} = mk⇔ (λ ())          proj₂
diff --git a/src/Data/Integer/Base.agda b/src/Data/Integer/Base.agda
index 8381402635..ba22b01de2 100644
--- a/src/Data/Integer/Base.agda
+++ b/src/Data/Integer/Base.agda
@@ -103,6 +103,19 @@ data _<_ : ℤ → ℤ → Set where
   -<+ : ∀ {m n} → -[1+ m ] < + n
   +<+ : ∀ {m n} → (m<n : m ℕ.< n) → + m < + n
 
+-- Destructors of _≤_, _<_
+-≤-⁻¹ : ∀ {m} {n} → -[1+ m ] ≤ -[1+ n ] → n ℕ.≤ m
+-≤-⁻¹ (-≤- n≤m) = n≤m
+
++≤+⁻¹ : ∀ {m} {n} → + m ≤ + n → m ℕ.≤ n
++≤+⁻¹ (+≤+ m≤n) = m≤n
+
+-<-⁻¹ : ∀ {m} {n} → -[1+ m ] < -[1+ n ] → n ℕ.< m
+-<-⁻¹ (-<- n<m) = n<m
+
++<+⁻¹ : ∀ {m} {n} → + m < + n → m ℕ.< n
++<+⁻¹ (+<+ m<n) = m<n
+
 _≥_ : Rel ℤ 0ℓ
 x ≥ y = y ≤ x
 
diff --git a/src/Data/Integer/DivMod.agda b/src/Data/Integer/DivMod.agda
index 3fac7aba69..cad8404ba3 100644
--- a/src/Data/Integer/DivMod.agda
+++ b/src/Data/Integer/DivMod.agda
@@ -8,16 +8,17 @@
 
 module Data.Integer.DivMod where
 
-open import Data.Integer.Base using (+_; -[1+_]; +[1+_]; NonZero; _%_; ∣_∣;
-  _%ℕ_; _/ℕ_; _+_; _*_; -_; _-_; pred; -1ℤ; 0ℤ; _⊖_; _≤_; _<_; +≤+; suc;
-  +<+)
+open import Data.Integer.Base
 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.DivMod as ℕ using (m≡m%n+[m/n]*n; m%n≤n; m%n<n; n/1≡n; n%1≡0;
+  m*n/m*o≡n/o; m*n%o≡m*n%[m*o])
+import Data.Nat.Properties as ℕ using (m∸n≤m; m*n≢0; m*n≢0⇒m≢0; m*n≢0⇒n≢0;
+  m*n≡0⇒n≡0; *-comm)
 open import Function.Base using (_∘′_)
 open import Relation.Binary.PropositionalEquality.Core
-  using (_≡_; cong; sym; subst)
+  using (_≡_; _≢_; refl; cong; sym; subst; trans; respʳ)
+open import Relation.Nullary.Negation using (contradiction)
 open ≤-Reasoning
 
 ------------------------------------------------------------------------
@@ -129,6 +130,120 @@ 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    ∎
 
+i/ℕ1≡i : ∀ i → i /ℕ 1 ≡ i
+i/ℕ1≡i (+ n) = cong +_ (ℕ.n/1≡n n)
+i/ℕ1≡i -[1+ n ] with ℕ.suc n ℕ.% 1 | ℕ.n%1≡0 (ℕ.suc n)
+... | ℕ.zero | suc[n]%1≡0 = cong (λ x → - (+ x)) (ℕ.n/1≡n (ℕ.suc n))
+
+i/1≡i : ∀ i → i / + 1 ≡ i
+i/1≡i i = trans (div-pos-is-/ℕ i 1) (i/ℕ1≡i i)
+
+/ℕ-congʳ : ∀ i {m} {n} .{{_ : ℕ.NonZero m}} → .{{_ : ℕ.NonZero n}} →
+           m ≡ n → i /ℕ m ≡ i /ℕ n
+/ℕ-congʳ i {m} {n} refl = refl
+
+nonNeg[i]⇒i/ℕd : ∀ i d .{{_ : ℕ.NonZero d}} .{{_ : NonNegative i}} →
+                i /ℕ d ≡ + (∣ i ∣ ℕ./ d)
+nonNeg[i]⇒i/ℕd (+ i) d = refl
+
+neg[i]∧∣i∣%d≡0⇒i/ℕd : ∀ i {d} .{{_ : ℕ.NonZero d}} .{{_ : Negative i}} →
+                     ∣ i ∣ ℕ.% d ≡ 0 → i /ℕ d ≡ - (+ (∣ i ∣ ℕ./ d))
+neg[i]∧∣i∣%d≡0⇒i/ℕd -[1+ n ] {d} _ with ℕ.zero ← ℕ.suc n ℕ.% d = refl
+
+neg[i]∧∣i∣%d≢0⇒i/ℕd : ∀ i d .{{_ : ℕ.NonZero d}} .{{_ : Negative i}}
+                     .{{_ : ℕ.NonZero (∣ i ∣ ℕ.% d)}} → i /ℕ d ≡ -[1+ ∣ i ∣ ℕ./ d ]
+neg[i]∧∣i∣%d≢0⇒i/ℕd -[1+ n ] d {{_}} {{_}} {{mod}} with ℕ.suc n ℕ.% d
+... | ℕ.zero  = contradiction refl (ℕ.≢-nonZero⁻¹ ℕ.zero)
+... | ℕ.suc _ = refl
+
+*-cancelˡ-/ℕ : ∀ m i n .{{_ : ℕ.NonZero n}} .{{_ : ℕ.NonZero (m ℕ.* n)}} →
+               (+ m * i) /ℕ (m ℕ.* n) ≡ i /ℕ n
+*-cancelˡ-/ℕ m i@(+ _) n = begin-equality
+  (+ m * i) /ℕ (m ℕ.* n)
+      ≡⟨ nonNeg[i]⇒i/ℕd (+ m * i) (m ℕ.* n) ⟩
+  + (∣ + m * i ∣ ℕ./ (m ℕ.* n))
+      ≡⟨ cong (+_ ∘′ (ℕ._/ (m ℕ.* n))) (∣i*j∣≡∣i∣*∣j∣ (+ m) i) ⟩
+  + ((m ℕ.* ∣ i ∣) ℕ./ (m ℕ.* n))
+      ≡⟨ cong +_ (ℕ.m*n/m*o≡n/o m ∣ i ∣ n) ⟩
+  + (∣ i ∣ ℕ./ n)
+      ≡⟨ nonNeg[i]⇒i/ℕd i n ⟨
+  i /ℕ n ∎
+  where
+    instance
+      _ : ℕ.NonZero m
+      _ = ℕ.m*n≢0⇒m≢0 m
+      _ : NonNegative (+ m * i)
+      _ = i≥0∧j≥0⇒i*j≥0 (+ m) i
+*-cancelˡ-/ℕ m i@(-[1+ _ ]) n = helper
+  where
+    m*[∣i∣%n]≡∣m*i∣%[m*n] : m ℕ.* (∣ i ∣ ℕ.% n) ≡ ∣ + m * i ∣ ℕ.% (m ℕ.* n)
+    m*[∣i∣%n]≡∣m*i∣%[m*n] = trans (ℕ.m*n%o≡m*n%[m*o] m ∣ i ∣ n)
+                                  (cong (ℕ._% (m ℕ.* n)) (sym (∣i*j∣≡∣i∣*∣j∣ (+ m) i)))
+    instance
+      _ : ℕ.NonZero m
+      _ = ℕ.m*n≢0⇒m≢0 m
+      _ : Positive (+ m)
+      _ = nonNeg∧nonZero⇒Pos (+ m)
+      _ : Negative (+ m * i)
+      _ = i>0∧j<0⇒i*j<0 (+ m) i
+    helper : (+ m * i) /ℕ (m ℕ.* n) ≡ i /ℕ n
+    helper with ∣ + m * i ∣ ℕ.% (m ℕ.* n) in ∣m*i∣%[m*n]
+    ... | ℕ.zero = begin-equality
+      (+ m * i) /ℕ (m ℕ.* n)
+          ≡⟨ neg[i]∧∣i∣%d≡0⇒i/ℕd (+ m * i) ∣m*i∣%[m*n] ⟩
+      - (+ (∣ + m * i ∣ ℕ./ (m ℕ.* n)))
+          ≡⟨ cong (-_ ∘′ +_ ∘′ (ℕ._/ _)) (∣i*j∣≡∣i∣*∣j∣ (+ m) i) ⟩
+      - (+ ((m ℕ.* ∣ i ∣) ℕ./ (m ℕ.* n)))
+          ≡⟨ cong (-_ ∘′ +_) (ℕ.m*n/m*o≡n/o m ∣ i ∣ n) ⟩
+      - (+ (∣ i ∣ ℕ./ n)) ≡⟨ neg[i]∧∣i∣%d≡0⇒i/ℕd i ∣i∣%m≡0 ⟨
+      i /ℕ n ∎
+      where
+        m*[∣i∣%n]≡0 : m ℕ.* (∣ i ∣ ℕ.% n) ≡ 0
+        m*[∣i∣%n]≡0 = trans m*[∣i∣%n]≡∣m*i∣%[m*n] ∣m*i∣%[m*n]
+        ∣i∣%m≡0 : ∣ i ∣ ℕ.% n ≡ 0
+        ∣i∣%m≡0 = ℕ.m*n≡0⇒n≡0 m _ m*[∣i∣%n]≡0
+    ... | ℕ.suc _ = begin-equality
+      (+ m * i) /ℕ (m ℕ.* n)
+          ≡⟨ neg[i]∧∣i∣%d≢0⇒i/ℕd (+ m * i) (m ℕ.* n) ⟩
+      -[1+ ∣ + m * i ∣ ℕ./ (m ℕ.* n) ]
+          ≡⟨ cong (-[1+_] ∘′ (ℕ._/ (m ℕ.* n))) (∣i*j∣≡∣i∣*∣j∣ (+ m) i) ⟩
+      -[1+ (m ℕ.* ∣ i ∣) ℕ./ (m ℕ.* n) ]
+          ≡⟨ cong -[1+_] (ℕ.m*n/m*o≡n/o m ∣ i ∣ n) ⟩
+      -[1+ ∣ i ∣ ℕ./ n ] ≡⟨ neg[i]∧∣i∣%d≢0⇒i/ℕd i n ⟨
+      i /ℕ n ∎
+      where instance
+        ∣m*i∣%[m*n]≢0 : ℕ.NonZero (∣ + m * i ∣ ℕ.% (m ℕ.* n))
+        ∣m*i∣%[m*n]≢0 rewrite ∣m*i∣%[m*n] = _
+        m*[∣i∣%n]≢0 : ℕ.NonZero (m ℕ.* (∣ i ∣ ℕ.% n))
+        m*[∣i∣%n]≢0 rewrite m*[∣i∣%n]≡∣m*i∣%[m*n] | ∣m*i∣%[m*n] = _
+        ∣i∣%n≢0 : ℕ.NonZero (∣ i ∣ ℕ.% n)
+        ∣i∣%n≢0 = ℕ.m*n≢0⇒n≢0 m
+
+*-cancelʳ-/ℕ : ∀ i m n .{{_ : ℕ.NonZero n}} .{{_ : ℕ.NonZero (n ℕ.* m)}} →
+               (i * + m) /ℕ (n ℕ.* m) ≡ i /ℕ n
+*-cancelʳ-/ℕ i m n rewrite *-comm i (+ m) | ℕ.*-comm n m = *-cancelˡ-/ℕ m i n
+
+*-cancelˡ-/ : ∀ i j k .{{_ : NonZero k}} .{{_ : NonZero (i * k)}} →
+              .{{_ : NonNegative i}} → (i * j) / (i * k) ≡ j / k
+*-cancelˡ-/ (+ i) j k = begin-equality
+  (sign (+ i * k) ◃ 1) * ((+ i * j) /ℕ ∣ + i * k ∣)
+        ≡⟨ cong (λ x → (x ◃ 1) * ((+ i * j) /ℕ _)) (sign-* (+ i) k)⟩
+  (sign k ◃ 1) * ((+ i * j) /ℕ ∣ + i * k ∣)
+        ≡⟨ cong ((sign k ◃ 1) *_) (/ℕ-congʳ (+ i * j) (∣i*j∣≡∣i∣*∣j∣ (+ i) k)) ⟩
+  (sign k ◃ 1) * ((+ i * j) /ℕ (∣ + i ∣ ℕ.* ∣ k ∣))
+        ≡⟨ cong ((sign k ◃ 1) *_) (*-cancelˡ-/ℕ i j ∣ k ∣) ⟩
+  j / k ∎
+  where
+    instance
+      _ : NonZero (+ i)
+      _ = i*j≢0⇒i≢0 (+ i)
+      _ : ℕ.NonZero (∣ + i ∣ ℕ.* ∣ k ∣)
+      _ = ℕ.m*n≢0 ∣ + i ∣ ∣ k ∣
+
+*-cancelʳ-/ : ∀ i j k .{{_ : NonZero k}} .{{_ : NonZero (k * j)}} →
+              .{{_ : NonNegative j}} → (i * j) / (k * j) ≡ i / k
+*-cancelʳ-/ i j k rewrite *-comm i j | *-comm k j = *-cancelˡ-/ j i k
+
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
 ------------------------------------------------------------------------
diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda
index 9740d50686..ec00f1ef95 100644
--- a/src/Data/Integer/Properties.agda
+++ b/src/Data/Integer/Properties.agda
@@ -36,12 +36,12 @@ open import Relation.Binary.Structures
 open import Relation.Binary.Definitions
   using (DecidableEquality; Reflexive; Transitive; Antisymmetric; Total; Decidable; Irrelevant; Irreflexive; Asymmetric; LeftTrans; RightTrans; Trichotomous; tri≈; tri<; tri>)
 open import Relation.Binary.PropositionalEquality.Core
-  using (_≡_; refl; cong; cong₂; sym; _≢_; subst; subst₂; resp₂; trans)
+  using (_≡_; refl; cong; cong₂; sym; _≢_; ≢-sym; subst; subst₂; resp₂; trans)
 open import Relation.Binary.PropositionalEquality.Properties
   using (module ≡-Reasoning; setoid; decSetoid; isEquivalence)
 open import Relation.Nullary.Decidable.Core using (yes; no)
 import Relation.Nullary.Reflects as Reflects
-open import Relation.Nullary.Negation.Core using (¬_; contradiction)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction; contraposition)
 import Relation.Nullary.Decidable as Dec
 
 open import Algebra.Definitions {A = ℤ} _≡_
@@ -407,9 +407,16 @@ nonPositive⁻¹ -[1+ n ] = -≤+
 nonNegative⁻¹ : ∀ i → .{{NonNegative i}} → i ≥ 0ℤ
 nonNegative⁻¹ (+ n) = +≤+ z≤n
 
+nonZero⁻¹ : ∀ i → .{{NonZero i}} → i ≢ 0ℤ
+nonZero⁻¹ (+ n) = contraposition +-injective (ℕ.≢-nonZero⁻¹ n)
+nonZero⁻¹ -[1+ n ] ()
+
 negative<positive : ∀ i j → .{{Negative i}} → .{{Positive j}} → i < j
 negative<positive i j = <-trans (negative⁻¹ i) (positive⁻¹ j)
 
+nonNeg∧nonZero⇒Pos : ∀ i → .{{NonNegative i}} → .{{NonZero i}} → Positive i
+nonNeg∧nonZero⇒Pos i = positive (≤∧≢⇒< (nonNegative⁻¹ i) (≢-sym (nonZero⁻¹ i)))
+
 ------------------------------------------------------------------------
 -- Properties of -_
 ------------------------------------------------------------------------
@@ -1169,6 +1176,9 @@ i-j≡0⇒i≡j i j i-j≡0 = begin
   0ℤ + j        ≡⟨  +-identityˡ j ⟩
   j             ∎ where open ≡-Reasoning
 
+∣i-j∣≡0⇒i≡j : ∀ {i} {j} → ∣ i - j ∣ ≡ 0 → i ≡ j
+∣i-j∣≡0⇒i≡j {i} {j} eq = i-j≡0⇒i≡j i j (∣i∣≡0⇒i≡0 eq)
+
 i≤j⇒i-k≤j : ∀ k .{{_ : NonNegative k}} → i ≤ j → i - k ≤ j
 i≤j⇒i-k≤j {i}         +0       i≤j rewrite +-identityʳ i = i≤j
 i≤j⇒i-k≤j {+ m}       +[1+ n ] i≤j = ≤-trans (m⊖n≤m m (suc n)) i≤j
@@ -1633,6 +1643,12 @@ i*j≡0⇒i≡0∨j≡0 i p with ℕ.m*n≡0⇒m≡0∨n≡0 ∣ i ∣ (abs-cong
 i*j≢0 : ∀ i j .{{_ : NonZero i}} .{{_ : NonZero j}} → NonZero (i * j)
 i*j≢0 i j rewrite abs-* i j = ℕ.m*n≢0 ∣ i ∣ ∣ j ∣
 
+i*j≢0⇒i≢0 : ∀ i {j} .{{_ : NonZero (i * j)}} → NonZero i
+i*j≢0⇒i≢0 i {j} rewrite abs-* i j = ℕ.m*n≢0⇒m≢0 ∣ i ∣
+
+i*j≢0⇒j≢0 : ∀ i {j} .{{_ : NonZero (i * j)}} → NonZero j
+i*j≢0⇒j≢0 i {j} rewrite abs-* i j = ℕ.m*n≢0⇒n≢0 ∣ i ∣
+
 ------------------------------------------------------------------------
 -- Properties of _^_
 ------------------------------------------------------------------------
@@ -1826,6 +1842,15 @@ neg-distribʳ-* i j = begin
 *-cancelʳ-<-neg : ∀ n → i * -[1+ n ] < j * -[1+ n ] → i > j
 *-cancelʳ-<-neg {i} {j} n = *-cancelʳ-<-nonPos -[1+ n ]
 
+------------------------------------------------------------------------
+-- Properties of _*_ and Positive/NonPositive/Negative/NonNegative
+
+i≥0∧j≥0⇒i*j≥0 : ∀ i j → .{{NonNegative i}} → .{{NonNegative j}} → NonNegative (i * j)
+i≥0∧j≥0⇒i*j≥0 i j = nonNegative (*-monoʳ-≤-nonNeg j (nonNegative⁻¹ i))
+
+i>0∧j<0⇒i*j<0 : ∀ i j → .{{Positive i}} → .{{Negative j}} → Negative (i * j)
+i>0∧j<0⇒i*j<0 i j = negative (*-monoʳ-<-neg j (positive⁻¹ i))
+
 ------------------------------------------------------------------------
 -- Properties of _*_ and ∣_∣
 
diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda
index 477acf0e14..5db943535d 100644
--- a/src/Data/Nat/DivMod.agda
+++ b/src/Data/Nat/DivMod.agda
@@ -450,6 +450,11 @@ m%n*o≡m*o%[n*o] m n o = 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≡m*n%[m*o] : ∀ m n o .{{_ : NonZero o}} .{{_ : NonZero (m * o)}} →
+                  m * (n % o) ≡ (m * n) % (m * o)
+m*n%o≡m*n%[m*o] m n o rewrite *-comm m (n % o) | *-comm m n | *-comm m o
+  = m%n*o≡m*o%[n*o] n o m
+
 [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) o<n = begin-equality
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index b94bf913ef..3ebd46860c 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -981,6 +981,9 @@ m*n≢0⇒n≢0 m {n} rewrite *-comm m n = m*n≢0⇒m≢0 n {m}
 m*n≡0⇒m≡0 : ∀ m n .{{_ : NonZero n}} → m * n ≡ 0 → m ≡ 0
 m*n≡0⇒m≡0 zero (suc _) eq = refl
 
+m*n≡0⇒n≡0 : ∀ m n .{{_ : NonZero m}} → m * n ≡ 0 → n ≡ 0
+m*n≡0⇒n≡0 (suc _) zero eq = refl
+
 m*n≡1⇒m≡1 : ∀ m n → m * n ≡ 1 → m ≡ 1
 m*n≡1⇒m≡1 (suc zero)    n          _  = refl
 m*n≡1⇒m≡1 (suc (suc m)) (suc zero) ()
diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda
index 0660b45f5a..5bdf520db4 100644
--- a/src/Data/Rational/Unnormalised/Properties.agda
+++ b/src/Data/Rational/Unnormalised/Properties.agda
@@ -26,13 +26,13 @@ open import Algebra.Construct.NaturalChoice.Base
   using (MaxOperator; MinOperator)
 import Algebra.Construct.NaturalChoice.MinMaxOp as MinMaxOp
 import Algebra.Lattice.Construct.NaturalChoice.MinMaxOp as LatticeMinMaxOp
-open import Data.Bool.Base using (T; true; false)
+open import Data.Bool.Base using (T; true; false; not)
+open import Data.Bool.Properties using (if-cong; T-to-≡; ≡-to-T; T-not-to-≡; ≡-to-T-not)
 open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Data.Nat.Base as ℕ using (suc; pred)
 import Data.Nat.Properties as ℕ
-  using (≤-refl; +-comm; +-identityʳ; +-assoc
-        ; *-identityʳ; *-comm; *-assoc; *-suc)
 open import Data.Integer.Base as ℤ using (ℤ; +0; +[1+_]; -[1+_]; 0ℤ; 1ℤ; -1ℤ)
+import Data.Integer.DivMod as ℤ
 open import Data.Integer.Solver renaming (module +-*-Solver to ℤ-solver)
 import Data.Integer.Properties as ℤ
 open import Data.Rational.Unnormalised.Base
@@ -41,8 +41,6 @@ open import Data.Sum.Base as Sum using (_⊎_; [_,_]′; inj₁; inj₂)
 import Data.Sign as Sign
 open import Function.Base using (_on_; _$_; _∘_; flip)
 open import Level using (0ℓ)
-open import Relation.Nullary.Decidable.Core as Dec using (yes; no)
-open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
 open import Relation.Binary.Bundles
   using (Setoid; DecSetoid; Preorder; TotalPreorder; Poset; TotalOrder
@@ -61,6 +59,10 @@ open import Relation.Binary.PropositionalEquality
 import Relation.Binary.Properties.Poset as PosetProperties
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 open import Relation.Binary.Reasoning.Syntax
+open import Relation.Nullary.Decidable.Core as Dec using (yes; no)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
+open import Relation.Nullary.Reflects
+  using (Reflects; fromEquivalence; reflects-false; reflects-refute)
 
 open import Algebra.Consequences.Propositional {A = ℚᵘ}
 open import Algebra.Properties.CommutativeSemigroup ℤ.*-commutativeSemigroup
@@ -406,6 +408,15 @@ antimono⇒cong = BC.antimono⇒cong _≃_ _≃_ ≃-sym ≤-reflexive ≤-antis
 ≤⇒≤ᵇ : p ≤ q → T (p ≤ᵇ q)
 ≤⇒≤ᵇ = ℤ.≤⇒≤ᵇ ∘ drop-*≤*
 
+≤ᵇ-reflects-≤ : ∀ p q → Reflects (p ≤ q) (p ≤ᵇ q)
+≤ᵇ-reflects-≤ p q = fromEquivalence ≤ᵇ⇒≤ ≤⇒≤ᵇ
+
+≰ᵇ⇒≰ : T (not (p ≤ᵇ q)) → p ≰ q
+≰ᵇ⇒≰ {p} {q} p≰ᵇq = reflects-false (≤ᵇ-reflects-≤ p q) (T-not-to-≡ p≰ᵇq)
+
+≰⇒≰ᵇ : p ≰ q → T (not (p ≤ᵇ q))
+≰⇒≰ᵇ {p} {q} p≰q = ≡-to-T-not (reflects-refute (≤ᵇ-reflects-≤ p q) p≰q)
+
 ------------------------------------------------------------------------
 -- Properties of _<_
 ------------------------------------------------------------------------
@@ -423,6 +434,15 @@ drop-*<* (*<* pq<qp) = pq<qp
 <⇒<ᵇ : p < q → T (p <ᵇ q)
 <⇒<ᵇ = ℤ.<⇒<ᵇ ∘ drop-*<*
 
+<ᵇ-reflects-< : ∀ p q → Reflects (p < q) (p <ᵇ q)
+<ᵇ-reflects-< p q = fromEquivalence <ᵇ⇒< <⇒<ᵇ
+
+≮ᵇ⇒≮ : T (not (p <ᵇ q)) → p ≮ q
+≮ᵇ⇒≮ {p} {q} p≮ᵇq = reflects-false (<ᵇ-reflects-< p q) (T-not-to-≡ p≮ᵇq)
+
+≮⇒≮ᵇ : p ≮ q → T (not (p <ᵇ q))
+≮⇒≮ᵇ {p} {q} p≮q = ≡-to-T-not (reflects-refute (<ᵇ-reflects-< p q) p≮q)
+
 ------------------------------------------------------------------------
 -- Relationship between other operators
 
@@ -938,6 +958,13 @@ nonNeg+nonNeg⇒nonNeg p q = nonNegative
   (p + 0ℚᵘ) - r       ≃⟨ +-congˡ (- r) (+-identityʳ p) ⟩
   p - r               ∎ where open ≤-Reasoning
 
+neg-distrib-minus : ∀ p q → - (p - q) ≡ q - p
+neg-distrib-minus p q = begin
+  - (p - q)     ≡⟨ neg-distrib-+ p (- q) ⟩
+  - p + - (- q) ≡⟨ cong (- p +_) (neg-involutive-≡ q) ⟩
+  - p + q       ≡⟨ +-comm-≡ (- p) q ⟩
+  q + - p       ∎ where open ≡-Reasoning
+
 p≃q⇒p-q≃0 : ∀ p q → p ≃ q → p - q ≃ 0ℚᵘ
 p≃q⇒p-q≃0 p q p≃q = begin-equality
   p - q ≃⟨ +-congˡ (- q) p≃q ⟩
@@ -1566,6 +1593,23 @@ 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 _/_
+
+/-cancelʳ-< : ∀ {i} {j} d .{{_ : ℕ.NonZero d}} → i / d < j / d → i ℤ.< j
+/-cancelʳ-< {i} {j} d@(suc _) (*<* i*d<j*d) = begin-strict
+  i           ≡⟨ ↥[n/d]≡n i d ⟨
+  (↥ (i / d)) <⟨ ℤ.*-cancelʳ-<-nonNeg (ℤ.+ d) i*d<j*d ⟩
+  (↥ (j / d)) ≡⟨ ↥[n/d]≡n j d ⟩
+  j           ∎ where open ℤ.≤-Reasoning
+
+/-cancelʳ-≤ : ∀ {i} {j} d .{{_ : ℕ.NonZero d}} → i / d ≤ j / d → i ℤ.≤ j
+/-cancelʳ-≤ {i} {j} d@(suc _) (*≤* i*d≤i*d) = begin
+  i           ≡⟨ ↥[n/d]≡n i d ⟨
+  (↥ (i / d)) ≤⟨ ℤ.*-cancelʳ-≤-pos _ _(ℤ.+ d) i*d≤i*d ⟩
+  (↥ (j / d)) ≡⟨ ↥[n/d]≡n j d ⟩
+  j           ∎ where open ℤ.≤-Reasoning
+
 ------------------------------------------------------------------------
 -- Properties of _⊓_ and _⊔_
 ------------------------------------------------------------------------
@@ -1909,6 +1953,18 @@ pos⊔pos⇒pos p q = positive (⊔-mono-< (positive⁻¹ p) (positive⁻¹ q))
   ∣ p ∣ + ∣   q ∣  ∎
   where open ≤-Reasoning
 
+∣p-q∣≤∣p-r∣+∣r-q∣ : ∀ p q r → ∣ p - q ∣ ≤ ∣ p - r ∣ + ∣ r - q ∣
+∣p-q∣≤∣p-r∣+∣r-q∣ p q r = begin
+  ∣ p - q ∣             ≃⟨ ∣-∣-cong (+-minus-telescope p r q) ⟨
+  ∣ (p - r) + (r - q) ∣ ≤⟨ ∣p+q∣≤∣p∣+∣q∣ (p - r) (r - q) ⟩
+  ∣ p - r ∣ + ∣ r - q ∣ ∎ where open ≤-Reasoning
+
+∣p-q∣≡∣q-p∣ : ∀ p q → ∣ p - q ∣ ≡ ∣ q - p ∣
+∣p-q∣≡∣q-p∣ p q = begin
+  ∣ p - q ∣     ≡⟨ ∣-p∣≡∣p∣ (p - q) ⟨
+  ∣ - (p - q) ∣ ≡⟨ cong ∣_∣ (neg-distrib-minus p q) ⟩
+  ∣ q - p ∣     ∎ where open ≡-Reasoning
+
 ∣p*q∣≡∣p∣*∣q∣ : ∀ p q → ∣ p * q ∣ ≡ ∣ p ∣ * ∣ q ∣
 ∣p*q∣≡∣p∣*∣q∣ p@record{} q@record{} = begin
   ∣ p * q ∣                                           ≡⟨⟩
@@ -1934,6 +1990,275 @@ pos⊔pos⇒pos p q = positive (⊔-mono-< (positive⁻¹ p) (positive⁻¹ q))
 ∣-∣-nonNeg (mkℚᵘ +0       _) = _
 ∣-∣-nonNeg (mkℚᵘ -[1+ _ ] _) = _
 
+-q≤p≤q⇒∣p∣≤q : ∀ {p q} → - q ≤ p → p ≤ q → ∣ p ∣ ≤ q
+-q≤p≤q⇒∣p∣≤q {p} {q} -q≤p p≤q with ∣p∣≡p∨∣p∣≡-p p
+... | inj₁ ∣p∣≡p  =  ≤-respˡ-≃ (≃-reflexive (sym ∣p∣≡p)) p≤q
+... | inj₂ ∣p∣≡-p = begin
+  ∣ p ∣   ≡⟨ ∣p∣≡-p ⟩
+  - p     ≤⟨ neg-mono-≤ -q≤p ⟩
+  - (- q) ≡⟨ neg-involutive-≡ q ⟩
+  q       ∎ where open ≤-Reasoning
+
+-q<p<q⇒∣p∣<q : ∀ {p q} → - q < p → p < q → ∣ p ∣ < q
+-q<p<q⇒∣p∣<q {p} {q} -q<p p<q with ∣p∣≡p∨∣p∣≡-p p
+... | inj₁ ∣p∣≡p  =  <-respˡ-≃ (≃-reflexive (sym ∣p∣≡p)) p<q
+... | inj₂ ∣p∣≡-p = begin-strict
+  ∣ p ∣   ≡⟨ ∣p∣≡-p ⟩
+  - p     <⟨ neg-mono-< -q<p ⟩
+  - (- q) ≡⟨ neg-involutive-≡ q ⟩
+  q       ∎ where open ≤-Reasoning
+
+------------------------------------------------------------------------
+-- Properties of Rounding functions
+
+floor-cong : ∀ {p} {q} → p ≃ q → ⌊ p ⌋ ≡ ⌊ q ⌋
+floor-cong {p@record{}} {q@record{}} (*≡* ↥p↧q≡↥q↧p) = begin
+  ↥ p ℤ./ ↧ p                     ≡⟨ ℤ.*-cancelʳ-/ (↥ p) (↧ q) (↧ p) ⟨
+  (↥ p ℤ.* ↧ q) ℤ./ (↧ p ℤ.* ↧ q) ≡⟨ cong (ℤ._/ (↧ p ℤ.* ↧ q)) ↥p↧q≡↥q↧p ⟩
+  (↥ q ℤ.* ↧ p) ℤ./ (↧ p ℤ.* ↧ q) ≡⟨ cong (ℤ._/ (↧ p ℤ.* ↧ q)) (ℤ.*-comm (↥ q) _)⟩
+  (↧ p ℤ.* ↥ q) ℤ./ (↧ p ℤ.* ↧ q) ≡⟨ ℤ.*-cancelˡ-/ (↧ p) (↥ q) (↧ q) ⟩
+  ↥ q ℤ./ ↧ q ∎ where open ≡-Reasoning
+
+ceiling-cong : ∀ {p} {q} → p ≃ q → ⌈ p ⌉ ≡ ⌈ q ⌉
+ceiling-cong {p@record{}} {q@record{}} eq = cong ℤ.-_ (floor-cong (-‿cong eq))
+
+round-cong : ∀ {p} {q} → p ≃ q → round p ≡ round q
+round-cong {p@record{}} {q@record{}} eq with p ≤ᵇ 0ℚᵘ in leq
+... | false = begin
+  ⌊ p + ½ ⌋ ≡⟨ floor-cong (+-congˡ ½ eq) ⟩
+  ⌊ q + ½ ⌋ ≡⟨ if-cong q≤ᵇ0≡false ⟨
+  round q   ∎
+  where
+    open ≡-Reasoning
+    0<q : 0ℚᵘ < q
+    0<q = <-respʳ-≃ eq ((≰⇒> ∘ ≰ᵇ⇒≰ ∘ ≡-to-T-not) leq)
+    q≤ᵇ0≡false : (q ≤ᵇ 0ℚᵘ) ≡ false
+    q≤ᵇ0≡false = T-not-to-≡ (≰⇒≰ᵇ (<⇒≱ 0<q))
+... | true = begin
+  ⌈ p - ½ ⌉ ≡⟨ ceiling-cong (+-congˡ (- ½) eq) ⟩
+  ⌈ q - ½ ⌉ ≡⟨ if-cong q≤ᵇ0≡true ⟨
+  round q   ∎
+  where
+    open ≡-Reasoning
+    q≤0 : q ≤ 0ℚᵘ
+    q≤0 =  ≤-respˡ-≃ eq (≤ᵇ⇒≤ (≡-to-T leq))
+    q≤ᵇ0≡true : (q ≤ᵇ 0ℚᵘ) ≡ true
+    q≤ᵇ0≡true = T-to-≡ (≤⇒≤ᵇ q≤0)
+
+⌊i/1⌋≡i : ∀ i → ⌊ i / 1 ⌋ ≡ i
+⌊i/1⌋≡i i = ℤ.i/1≡i i
+
+⌈i/1⌉≡i : ∀ i → ⌈ i / 1 ⌉ ≡ i
+⌈i/1⌉≡i i = trans (cong ℤ.-_ (⌊i/1⌋≡i (ℤ.- i))) (ℤ.neg-involutive i)
+
+⌊-q⌋≡-⌈q⌉ : ∀ q → ⌊ - q ⌋ ≡ ℤ.- ⌈ q ⌉
+⌊-q⌋≡-⌈q⌉ q@record{} = sym (ℤ.neg-involutive ⌊ - q ⌋)
+
+⌈-q⌉≡-⌊q⌋ : ∀ q → ⌈ - q ⌉ ≡ ℤ.- ⌊ q ⌋
+⌈-q⌉≡-⌊q⌋ q@record{} = cong (λ x → ℤ.- ⌊ x ⌋) (neg-involutive-≡ q)
+
+private
+  q>0⇒round[-q]≡round[q] : ∀ {q} → q > 0ℚᵘ → round (- q) ≡ ℤ.- round q
+  q>0⇒round[-q]≡round[q] {q} q>0 = begin
+    round (- q)   ≡⟨ if-cong -q≤0 ⟩
+    ⌈ - q - ½ ⌉   ≡⟨ cong ceiling (neg-distrib-+ q ½) ⟨
+    ⌈ - (q + ½) ⌉ ≡⟨ ⌈-q⌉≡-⌊q⌋ (q + ½) ⟩
+    ℤ.- ⌊ q + ½ ⌋ ≡⟨ cong ℤ.-_ (if-cong q≥0) ⟨
+    ℤ.- round q   ∎
+    where
+    open ≡-Reasoning
+    -q≤0 : (- q ≤ᵇ 0ℚᵘ) ≡ true
+    -q≤0 = T-to-≡ (≤⇒≤ᵇ (<⇒≤ (neg-mono-< q>0)))
+    q≥0 : (q ≤ᵇ 0ℚᵘ) ≡ false
+    q≥0 = T-not-to-≡ (≰⇒≰ᵇ (<⇒≱ q>0))
+
+round[-q]≡-round[q] : ∀ q → round (- q) ≡ ℤ.- (round q)
+round[-q]≡-round[q] q@record{} with <-cmp q 0ℚᵘ
+... | tri< a ¬b ¬c = begin
+  round (- q)           ≡⟨ ℤ.neg-involutive (round (- q)) ⟨
+  ℤ.- (ℤ.- round (- q)) ≡⟨ cong ℤ.-_ (q>0⇒round[-q]≡round[q] (neg-mono-< a)) ⟨
+  ℤ.- round (- (- q))   ≡⟨ cong (ℤ.-_ ∘ round) (neg-involutive-≡ q) ⟩
+  ℤ.- round q           ∎ where open ≡-Reasoning
+... | tri≈ ¬a b ¬c = begin
+  round (- q) ≡⟨ round-cong (-‿cong b) ⟩
+  ℤ.- 0ℤ      ≡⟨ cong ℤ.-_ (round-cong b) ⟨
+  ℤ.- round q ∎ where open ≡-Reasoning
+... | tri> ¬a ¬b c = q>0⇒round[-q]≡round[q] c
+
+------------------------------------------------------------------------
+-- Bounds of ⌊_⌋ and ⌈_⌉
+
+⌊q⌋≤q : ∀ q → ⌊ q ⌋ / 1 ≤ q
+⌊q⌋≤q q@record{} = *≤* (begin
+  ⌊ q ⌋ ℤ.* (↧ q)           ≤⟨ ℤ.[n/d]*d≤n (↥ q) (↧ q) ⟩
+  (↥ q)                     ≡⟨ ℤ.*-identityʳ (↥ q) ⟨
+  (↥ q) ℤ.* (↧ (⌊ q ⌋ / 1)) ∎) where open ℤ.≤-Reasoning
+
+q<⌊q⌋+1 : ∀ q → q < ⌊ q ⌋ / 1 + 1ℚᵘ
+q<⌊q⌋+1 q@record{} = let n = ↥ q; d = ↧ q in *<* ( begin-strict
+  n ℤ.* 1ℤ                      ≡⟨ ℤ.*-identityʳ n ⟩
+  n                             ≡⟨ ℤ.a≡a%n+[a/n]*n n d  ⟩
+  ℤ.+ (n ℤ.% d) ℤ.+ ⌊ q ⌋ ℤ.* d <⟨ ℤ.+-monoˡ-< (⌊ q ⌋ ℤ.* d) (ℤ.+<+ (ℤ.n%d<d n d)) ⟩
+  d ℤ.+ ⌊ q ⌋ ℤ.* d             ≡⟨ i+j*i≡[j*1+1]i d ⌊ q ⌋ ⟩
+  ↥ (⌊ q ⌋ / 1 + 1ℚᵘ) ℤ.* d     ∎)
+  where
+    open ℤ.≤-Reasoning
+    i+j*i≡[j*1+1]i : ∀ i j → i ℤ.+ j ℤ.* i ≡ (j ℤ.* 1ℤ ℤ.+ 1ℤ) ℤ.* i
+    i+j*i≡[j*1+1]i i j rewrite ℤ.*-identityʳ j = begin-equality
+      i ℤ.+ j ℤ.* i        ≡⟨ cong (ℤ._+ j ℤ.* i) (ℤ.*-identityˡ i) ⟨
+      1ℤ ℤ.* i ℤ.+ j ℤ.* i ≡⟨ ℤ.*-distribʳ-+ i 1ℤ j ⟨
+      (1ℤ ℤ.+ j) ℤ.* i     ≡⟨ cong (ℤ._* i) (ℤ.+-comm 1ℤ j) ⟩
+      (j ℤ.+ 1ℤ) ℤ.* i     ∎
+
+q≤⌈q⌉ : ∀ q → q ≤ ⌈ q ⌉ / 1
+q≤⌈q⌉ q@record{} = begin
+  q         ≡⟨ neg-involutive-≡ q ⟨
+  - (- q)   ≤⟨ neg-mono-≤ (⌊q⌋≤q (- q)) ⟩
+  ⌈ q ⌉ / 1 ∎ where open ≤-Reasoning
+
+⌈q⌉-1<q : ∀ q → ⌈ q ⌉ / 1 - 1ℚᵘ < q
+⌈q⌉-1<q q@record{} = neg-cancel-< (begin-strict
+  - q                       <⟨ q<⌊q⌋+1 (- q) ⟩
+  ⌊ - q ⌋ / 1 + 1ℚᵘ         ≡⟨ neg-involutive-≡ (⌊ - q ⌋ / 1 + 1ℚᵘ) ⟨
+  - (- (⌊ - q ⌋ / 1 + 1ℚᵘ)) ≡⟨ cong -_ (neg-distrib-+ (⌊ - q ⌋ / 1) 1ℚᵘ) ⟩
+  - (⌈ q ⌉ / 1 - 1ℚᵘ)       ∎) where open ≤-Reasoning
+
+⌈q⌉≤⌊q⌋+1 : ∀ q → ⌈ q ⌉ ℤ.≤ ⌊ q ⌋ ℤ.+ 1ℤ
+⌈q⌉≤⌊q⌋+1 q = begin
+  ⌈ q ⌉                ≡⟨ \\-leftDividesˡ 1ℤ ⌈ q ⌉ ⟨
+  ℤ.suc (ℤ.pred ⌈ q ⌉) ≡⟨ cong ℤ.suc (ℤ.+-comm (ℤ.- 1ℤ) ⌈ q ⌉) ⟩
+  ℤ.suc (⌈ q ⌉ ℤ.- 1ℤ) ≤⟨ ℤ.i<j⇒suc[i]≤j ⌈q⌉-1<⌊q⌋+1 ⟩
+  ⌊ q ⌋ ℤ.+ 1ℤ         ∎
+  where
+  open ℤ.≤-Reasoning
+  open import Algebra.Properties.AbelianGroup ℤ.+-0-abelianGroup
+  ⌈q⌉-1<⌊q⌋+1 : ⌈ q ⌉ ℤ.- 1ℤ ℤ.< ⌊ q ⌋ ℤ.+ 1ℤ
+  ⌈q⌉-1<⌊q⌋+1 = begin-strict
+    ⌈ q ⌉ ℤ.- 1ℤ               ≡⟨ cong₂ ℤ._-_ (ℤ.*-identityʳ ⌈ q ⌉)
+                                              (ℤ.*-identityʳ 1ℤ) ⟨
+    ⌈ q ⌉ ℤ.* 1ℤ ℤ.- 1ℤ ℤ.* 1ℤ <⟨ /-cancelʳ-< 1 (<-trans (⌈q⌉-1<q q) (q<⌊q⌋+1 q)) ⟩
+    ⌊ q ⌋ ℤ.* 1ℤ ℤ.+ 1ℤ ℤ.* 1ℤ ≡⟨ cong₂ ℤ._+_ (ℤ.*-identityʳ ⌊ q ⌋)
+                                              (ℤ.*-identityʳ 1ℤ) ⟩
+    ⌊ q ⌋ ℤ.+ 1ℤ               ∎
+
+------------------------------------------------------------------------
+-- Approximation errors of ⌊_⌋ ⌈_⌉ and round(_)
+
+∣q-⌊q⌋∣<1 : ∀ q → ∣ q - ⌊ q ⌋ / 1 ∣ < 1ℚᵘ
+∣q-⌊q⌋∣<1 q = -q<p<q⇒∣p∣<q -1<q-⌊q⌋ q-⌊q⌋<1
+  where
+  open ≤-Reasoning
+  open import Algebra.Properties.AbelianGroup +-0-abelianGroup
+  -1<q-⌊q⌋ : - 1ℚᵘ < q - ⌊ q ⌋ / 1
+  -1<q-⌊q⌋ = let ⌊q⌋ = ⌊ q ⌋ / 1 in begin-strict
+    - 1ℚᵘ     <⟨ *<* ℤ.-<+ ⟩
+    0ℚᵘ       ≃⟨ +-inverseʳ ⌊q⌋ ⟨
+    ⌊q⌋ - ⌊q⌋ ≤⟨ +-monoˡ-≤ _ (⌊q⌋≤q q) ⟩
+    q - ⌊q⌋   ∎
+
+  q-⌊q⌋<1 : q - ⌊ q ⌋ / 1 < 1ℚᵘ
+  q-⌊q⌋<1 = let ⌊q⌋ = ⌊ q ⌋ / 1 in begin-strict
+    q - ⌊q⌋         <⟨ +-monoˡ-< _ (q<⌊q⌋+1 q) ⟩
+    ⌊q⌋ + 1ℚᵘ - ⌊q⌋ ≃⟨ xyx⁻¹≈y ⌊q⌋ 1ℚᵘ ⟩
+    1ℚᵘ             ∎
+
+∣q-⌈q⌉∣<1 : ∀ q → ∣ q - ⌈ q ⌉ / 1 ∣ < 1ℚᵘ
+∣q-⌈q⌉∣<1 q@record{} = let ⌊-q⌋ = ⌊ - q ⌋ / 1 in begin-strict
+  ∣ q - ⌈ q ⌉ / 1 ∣ ≡⟨ cong (λ x → ∣ q + x / 1 ∣) (⌊-q⌋≡-⌈q⌉ q) ⟨
+  ∣ q + ⌊-q⌋ ∣      ≡⟨ ∣-p∣≡∣p∣ (q + ⌊-q⌋) ⟨
+  ∣ - (q + ⌊-q⌋) ∣  ≡⟨ cong ∣_∣ (neg-distrib-+ q ⌊-q⌋) ⟩
+  ∣ - q - ⌊-q⌋ ∣    <⟨ ∣q-⌊q⌋∣<1 (- q) ⟩
+  1ℚᵘ               ∎ where open ≤-Reasoning
+
+∣q-round[q]∣≤½ : ∀ q → ∣ q - (round q) / 1 ∣ ≤ ½
+∣q-round[q]∣≤½ q = -q≤p≤q⇒∣p∣≤q -½≤q-round[q] (q-round[q]≤½ q)
+  where
+    open ≤-Reasoning
+    open import Algebra.Properties.AbelianGroup +-0-abelianGroup
+    q-round[q]≤½ : ∀ q → q - round q / 1 ≤ ½
+    q-round[q]≤½ q with q ≤ᵇ 0ℚᵘ
+    ... | false = let ⌊q+½⌋ = ⌊ q + ½ ⌋ / 1 in begin
+      q - ⌊q+½⌋               ≃⟨ +-congˡ _ (//-rightDividesʳ ½ q) ⟨
+      q + ½ - ½ - ⌊q+½⌋       <⟨ +-monoˡ-< _ (+-monoˡ-< _ (q<⌊q⌋+1 (q + ½))) ⟩
+      ⌊q+½⌋ + 1ℚᵘ - ½ - ⌊q+½⌋ ≃⟨ +-congˡ (- ⌊q+½⌋) (+-assoc ⌊q+½⌋ 1ℚᵘ (- ½)) ⟩
+      ⌊q+½⌋ + ½ - ⌊q+½⌋       ≃⟨ xyx⁻¹≈y ⌊q+½⌋ ½ ⟩
+      ½                       ∎
+    ... | true = begin
+      q - ⌈ q - ½ ⌉ / 1      ≡⟨ cong (λ x → q + x / 1) (⌊-q⌋≡-⌈q⌉ (q - ½)) ⟨
+      q + ⌊ - (q - ½) ⌋ / 1  ≤⟨ +-monoʳ-≤ q (⌊q⌋≤q (- (q - ½))) ⟩
+      q - (q - ½)            ≃⟨ +-congʳ q (⁻¹-anti-homo‿- q ½) ⟩
+      q + (½ - q)            ≡⟨ +-assoc-≡ q ½ (- q) ⟨
+      q + ½ - q              ≃⟨ xyx⁻¹≈y q ½ ⟩
+      ½                      ∎
+    -½≤q-round[q] : - ½ ≤ q - round q / 1
+    -½≤q-round[q] = begin
+      - ½ ≤⟨ neg-mono-≤ (q-round[q]≤½ (- q)) ⟩
+      - (- q - round (- q) / 1)
+          ≡⟨ neg-distrib-+ (- q) _ ⟩
+      - (- q) - (- (round (- q) / 1))
+          ≡⟨ cong₂ _+_ (neg-involutive-≡ q) (neg-involutive-≡ _)  ⟩
+      q + round (- q) / 1
+          ≡⟨ cong ((q +_) ∘ (_/ 1)) (round[-q]≡-round[q] q) ⟩
+      q + ℤ.- round q / 1 ∎
+
+i≤q⇒i≤⌊q⌋ : ∀ i q → i / 1 ≤ q → i ℤ.≤ ⌊ q ⌋
+i≤q⇒i≤⌊q⌋ i q i/1≤q = begin
+  i                    ≤⟨ ℤ.i<j⇒i≤pred[j] i<s⌊q⌋ ⟩
+  ℤ.pred (ℤ.suc ⌊ q ⌋) ≡⟨ ℤ.pred-suc ⌊ q ⌋ ⟩
+  ⌊ q ⌋                ∎
+  where
+  open ℤ.≤-Reasoning
+  i<s⌊q⌋ : i ℤ.< ℤ.suc ⌊ q ⌋
+  i<s⌊q⌋ = begin-strict
+    i                          <⟨ /-cancelʳ-< 1 (≤-<-trans i/1≤q (q<⌊q⌋+1 q)) ⟩
+    ⌊ q ⌋ ℤ.* 1ℤ ℤ.+ 1ℤ ℤ.* 1ℤ ≡⟨ cong₂ ℤ._+_ (ℤ.*-identityʳ ⌊ q ⌋)
+                                              (ℤ.*-identityʳ 1ℤ) ⟩
+    ⌊ q ⌋ ℤ.+ 1ℤ               ≡⟨ ℤ.+-comm ⌊ q ⌋ 1ℤ ⟩
+    ℤ.suc ⌊ q ⌋                ∎
+
+q≤i⇒⌈q⌉≤i : ∀ i q → q ≤ i / 1 → ⌈ q ⌉ ℤ.≤ i
+q≤i⇒⌈q⌉≤i i q q≤i/1 = begin
+  ⌈ q ⌉                ≡⟨ ℤ.suc-pred ⌈ q ⌉ ⟨
+  ℤ.suc (ℤ.pred ⌈ q ⌉) ≤⟨ ℤ.i<j⇒suc[i]≤j p⌊q⌋<i ⟩
+  i                    ∎
+  where
+  open ℤ.≤-Reasoning
+  p⌊q⌋<i : ℤ.pred ⌈ q ⌉ ℤ.< i
+  p⌊q⌋<i = begin-strict
+    ℤ.pred ⌈ q ⌉                     ≡⟨ ℤ.+-comm (ℤ.- 1ℤ) ⌈ q ⌉ ⟩
+    ⌈ q ⌉ ℤ.- 1ℤ                     ≡⟨ cong₂ ℤ._+_ (ℤ.*-identityʳ ⌈ q ⌉)
+                                                    (ℤ.*-identityʳ (ℤ.- 1ℤ)) ⟨
+    ⌈ q ⌉ ℤ.* 1ℤ ℤ.+ (ℤ.- 1ℤ) ℤ.* 1ℤ <⟨ /-cancelʳ-< 1 (<-≤-trans (⌈q⌉-1<q q) q≤i/1) ⟩
+    i                                ∎
+
+∣q-round[q]∣≤∣q-i∣ : ∀ q i → ∣ q - (round q) / 1 ∣ ≤ ∣ q - i / 1 ∣
+∣q-round[q]∣≤∣q-i∣ q@record{} i with ∣ q - i / 1 ∣ <ᵇ ½ in ∣q-i∣<½?
+... | false = ≤-trans (∣q-round[q]∣≤½ q) ½≤∣q-i∣
+  where
+    ½≤∣q-i∣ : ½ ≤ ∣ q - i / 1 ∣
+    ½≤∣q-i∣ = ≮⇒≥ (≮ᵇ⇒≮ (≡-to-T-not ∣q-i∣<½?))
+... | true = ≤-reflexive-≡ (cong (λ x → ∣ q - x / 1 ∣) round[q]≡i)
+  where
+    ∣q-i∣<½ : ∣ q - i / 1 ∣ < ½
+    ∣q-i∣<½ = <ᵇ⇒< (≡-to-T ∣q-i∣<½?)
+    ∣round[q]-i∣<1ℚᵘ : ∣ (round q) / 1 - i / 1 ∣ < 1ℚᵘ
+    ∣round[q]-i∣<1ℚᵘ = let round[q] = round q / 1 in begin-strict
+      ∣ round[q] - i / 1 ∣             ≤⟨ ∣p-q∣≤∣p-r∣+∣r-q∣ (round[q]) (i / 1) q ⟩
+      ∣ round[q] - q ∣ + ∣ q - i / 1 ∣ <⟨ +-monoʳ-< ∣ round[q] - q ∣ ∣q-i∣<½ ⟩
+      ∣ round[q] - q ∣ + ½             ≡⟨ cong (_+ ½) (∣p-q∣≡∣q-p∣ (round[q]) q) ⟩
+      ∣ q - round[q] ∣ + ½             ≤⟨ +-monoˡ-≤ ½ (∣q-round[q]∣≤½ q) ⟩
+      ½ + ½                            ≃⟨ *≡* refl ⟩
+      1ℚᵘ                              ∎ where open ≤-Reasoning
+    ∣round[q]-i∣<1ℕ : ℤ.∣ round q ℤ.- i ∣ ℕ.< 1
+    ∣round[q]-i∣<1ℕ = begin-strict
+      ℤ.∣ round q ℤ.- i ∣ ≡⟨ cong₂ (λ x y → ℤ.∣ x ℤ.+ y ∣)
+                                   (ℤ.*-identityʳ (round q))
+                                   (ℤ.*-identityʳ (ℤ.- i)) ⟨
+      ℤ.∣ round q ℤ.* 1ℤ ℤ.+ ℤ.- i ℤ.* 1ℤ ∣
+                          <⟨ ℤ.+<+⁻¹ (/-cancelʳ-< 1 ∣round[q]-i∣<1ℚᵘ) ⟩
+      1                   ∎ where open ℕ.≤-Reasoning
+    round[q]≡i : round q ≡ i
+    round[q]≡i = ℤ.∣i-j∣≡0⇒i≡j (ℕ.n<1⇒n≡0 ∣round[q]-i∣<1ℕ)
 
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda
index bd2c4600a8..8af6fd92e7 100644
--- a/src/Relation/Nullary/Reflects.agda
+++ b/src/Relation/Nullary/Reflects.agda
@@ -121,3 +121,17 @@ det (ofⁿ ¬a) (ofⁿ  _) = refl
 
 T-reflects-elim : ∀ {a b} → Reflects (T a) b → b ≡ a
 T-reflects-elim {a} r = det r (T-reflects a)
+
+reflects-true : ∀ {b} → Reflects A b → b ≡ true → A
+reflects-true (ofʸ a) eq = a
+
+reflects-false : ∀ {b} → Reflects A b → b ≡ false → ¬ A
+reflects-false (ofⁿ ¬a) eq = ¬a
+
+reflects-proof : ∀ {b} → Reflects A b → A → b ≡ true
+reflects-proof (ofʸ a₁) a = refl
+reflects-proof (ofⁿ ¬a) a = contradiction a ¬a
+
+reflects-refute : ∀ {b} → Reflects A b → ¬ A → b ≡ false
+reflects-refute (ofʸ a) ¬a = contradiction a ¬a
+reflects-refute (ofⁿ ¬a₁) ¬a = refl