added alias for equality

jamesmckinna · Dec 14, 2023 · 70c43b4 · 70c43b4
1 parent 9838568
commit 70c43b4
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 0 deletions.
diff --git 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
@@ -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