From 37c11d55ba713bfe24db04437fbc19f798a8bdcd Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 24 Jan 2025 13:52:31 +0000
Subject: [PATCH] actually add the consequence to `CHANGELOG`

---
 CHANGELOG.md | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index b047b3e217..900a4c3f08 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -57,6 +57,12 @@ New modules
 Additions to existing modules
 -----------------------------
 
+* In `Algebra.Consequences.Base`:
+  ```agda
+  integral⇒noZeroDivisors : Integral _≈_ 1# 0# _•_ → ¬ (1# ≈ 0#) →
+                            NoZeroDivisors _≈_ 0# _•_
+  ```
+
 * In `Algebra.Construct.Pointwise`:
   ```agda
   isNearSemiring                  : IsNearSemiring _≈_ _+_ _*_ 0# →