fix

math-comp · Sep 27, 2023 · 85c5795 · 85c5795
1 parent ca70a30
commit 85c5795
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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
@@ -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.