diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 542d716f8..21d230e99 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -43,6 +43,9 @@
   + lemmas `lteD2rE`, `leeD2rE`
   + lemmas `lte_dD2rE`, `lee_dD2rE`
 
+- in `mathcomp_extra.v`:
+  + lemma `invf_ltp`
+
 ### Changed
 
 - in `topology.v`: