diff --git a/CHANGELOG.md b/CHANGELOG.md
index bb6e91c887..1be5e109d4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -44,6 +44,11 @@ Non-backwards compatible changes
   As a result many of the `Composition` lemmas now take a proof of
   transitivity and the `Identity` lemmas now take a proof of reflexivity.
 
+* The implementation of `≤-total` in `Data.Nat.Properties` has been altered
+  to use operations backed by primitives, rather than recursion, making it
+  significantly faster. However, its reduction behaviour on open terms may have
+  changed.
+
 * The module `IO.Primitive` was moved to `IO.Primitive.Core`.
 
 Minor improvements