diff --git a/CHANGELOG.md b/CHANGELOG.md
index a76d349d39..c0d795f443 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -45,6 +45,7 @@ Additions to existing modules
   ```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
diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda
index 5933d6ea6f..abac2915a7 100644
--- a/src/Data/Nat/Divisibility.agda
+++ b/src/Data/Nat/Divisibility.agda
@@ -42,6 +42,9 @@ 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