From b21ee0c664a8efcec622851bb91097d6c4bd2634 Mon Sep 17 00:00:00 2001
From: Takafumi Saikawa <tscompor@gmail.com>
Date: Wed, 18 Dec 2024 15:57:58 +0900
Subject: [PATCH] undo eq_lt_total and le_lt_total

---
 CHANGELOG_UNRELEASED.md | 3 ---
 1 file changed, 3 deletions(-)

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`