diff --git a/CHANGELOG.md b/CHANGELOG.md
index 675d45893334fd5883ebc1cafedde0b0af64bf1a..c0e89c6f86a384b988a05e84e9f52cd1677efcb9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -28,6 +28,9 @@ lemma.
 * Change `WP` notation to allow type annotations and (exhaustive) patterns for
   the return value binder.
 * Rename `bi.lib.fixpoint` module to `bi.lib.fixpoint_mono`.
+* Add `bi.lib.fixpoint_banach` module with lemmas for proving that a `fixpoint`
+  (of a contractive function) is persistent/affine/etc. (with help from William
+  Mansky)
 
 **Changes in `heap_lang`:**