[Add] Properties of rounding in Rational

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

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₂

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
 

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
 ------------------------------------------------------------------------