diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4b39ffc11365b45966c44230dc8e9b8a5c67bae9..e27b0657b4ff427b7dbeff4310997ed80db4e81e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -28,6 +28,8 @@ lot to everyone involved!
 - Add some more lemmas about `Finite` and `pred_finite`.
 - Add lemmas about `last`: `last_app_cons`, `last_app`, `last_Some`, and
   `last_Some_elem_of`.
+- Add versions of Pigeonhole principle for Finite types, natural numbers, and
+  lists.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).