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.
diff --git a/theories/hoelder.v b/theories/hoelder.v
index 4d958e0527..78a0296f7a 100644
--- a/theories/hoelder.v
+++ b/theories/hoelder.v
@@ -300,9 +300,9 @@ have [->|w20] := eqVneq w2 0.
   by rewrite lt_neqAle eq_sym onem_ge0// andbT.
 have [->|p_neq1] := eqVneq p 1.
   by rewrite !powRr1// addr_ge0// mulr_ge0// /w2 ?onem_ge0.
-have {p1 p_neq1}p1 : 1 < p by rewrite lt_neqAle eq_sym p_neq1.
+have {p_neq1} {}p1 : 1 < p by rewrite lt_neqAle eq_sym p_neq1.
 pose q := p / (p - 1).
-have q1 : 1 <= q by rewrite /q ler_pdivl_mulr// ?mul1r ?lerBr// subr_gt0.
+have q1 : 1 <= q by rewrite /q ler_pdivl_mulr// ?mul1r ?gerBl// subr_gt0.
 have q0 : 0 < q by rewrite (lt_le_trans _ q1).
 have pq1 : p^-1 + q^-1 = 1.
   rewrite /q invf_div -{1}(div1r p) -mulrDl addrCA subrr addr0.