diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 9c9b32047..e3d40e76f 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -4,9 +4,6 @@
 
 ### Added
 
-- in file `mathcomp_extra.v`,
-  + lemmas `eq_lt_total`, `le_lt_total`
-
 - file `Rstruct_topology.v`
 
 - package `coq-mathcomp-reals` depending on `coq-mathcomp-classical`