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.