From 85c5795fa80b06e6295c698ad3e909c824517144 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Wed, 27 Sep 2023 19:27:58 +0900
Subject: [PATCH] fix

---
 CHANGELOG_UNRELEASED.md    | 2 +-
 classical/mathcomp_extra.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index a600e6b5e7..4f30cb93fc 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -83,7 +83,7 @@
   + lemma `ge0_integral_count`
 
 - in `mathcomp_extra.v`:
-  + lemma `lerBr`
+  + lemma `gerBl`
 
 ### Changed
 
diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
index 3a55a78137..c2ead7e4a2 100644
--- a/classical/mathcomp_extra.v
+++ b/classical/mathcomp_extra.v
@@ -1440,5 +1440,5 @@ End bigmax_seq.
 Arguments le_bigmax_seq {d T} x {I r} i0 P.
 
 (* NB: PR 1079 to MathComp in progress *)
-Lemma lerBr {R : numDomainType} (x y : R) : 0 <= y -> x - y <= x.
+Lemma gerBl {R : numDomainType} (x y : R) : 0 <= y -> x - y <= x.
 Proof. by move=> y0; rewrite ler_subl_addl ler_addr. Qed.