From b5dfe479b5a095936c2ee82f74e2ec7fe660162b Mon Sep 17 00:00:00 2001
From: Takafumi Saikawa <tscompor@gmail.com>
Date: Tue, 4 Feb 2025 23:16:22 +0900
Subject: [PATCH] rename ge0r to ger0

---
 CHANGELOG_UNRELEASED.md |  7 ++-----
 theories/derive.v       | 10 +++++-----
 2 files changed, 7 insertions(+), 10 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 784fa44a9..b63f2eda7 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -48,12 +48,9 @@
            `decr_derive1_le0_itvy`, `decr_derive1_le0_itvNy`,
            `incr_derive1_ge0`, `incr_derive1_ge0_itv`,
            `incr_derive1_ge0_itvy`, `incr_derive1_ge0_itvNy`,
-  + lemmas `ler0_derive1_nincry`, `le0r_derive1_ndecry`,
-           `ler0_derive1_nincrNy`, `le0r_derive1_ndecrNy`
- 
+  + lemmas `ler0_derive1_nincry`, `ger0_derive1_ndecry`,
+           `ler0_derive1_nincrNy`, `ger0_derive1_ndecrNy`
   + lemmas `ltr0_derive1_decr`, `gtr0_derive1_incr`
-  + lemmas `decr_derive1_le0`, `decr_derive1_le0_itv`
-  + lemmas `ler0_derive1_nincry`, `ge0r_derive1_ndecry`
 
 ### Changed
 
diff --git a/theories/derive.v b/theories/derive.v
index 97bd5374f..80585e3b9 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -1703,7 +1703,7 @@ apply: (@ler0_derive1_nincr _ _ N b) => //.
   by rewrite num_real.
 Unshelve. all: end_near. Qed.
 
-Lemma ge0r_derive1_ndecr (R : realType) (f : R -> R) (a b : R) :
+Lemma ger0_derive1_ndecr (R : realType) (f : R -> R) (a b : R) :
   (forall x, x \in `]a, b[%R -> derivable f x 1) ->
   (forall x, x \in `]a, b[%R -> 0 <= f^`() x) ->
   {within `[a,b], continuous f} ->
@@ -1716,10 +1716,10 @@ apply (@ler0_derive1_nincr _ (- f)) => t tab; first exact/derivableN/fdrvbl.
 by apply: continuousN; exact: fcont.
 Qed.
 #[deprecated(since="mathcomp-analysis 1.9.0",
-  note="renamed to `ge0r_derive1_ndecr`")]
-Notation le0r_derive1_ndecr := ge0r_derive1_ndecr (only parsing).
+  note="renamed to `ger0_derive1_ndecr`")]
+Notation le0r_derive1_ndecr := ger0_derive1_ndecr (only parsing).
 
-Lemma ge0r_derive1_ndecry {R : realType} (f : R -> R) (a b : R) :
+Lemma ger0_derive1_ndecry {R : realType} (f : R -> R) (a b : R) :
   (forall x, x \in `]a, +oo[%R -> derivable f x 1) ->
   (forall x, x \in `]a, +oo[%R -> 0 <= f^`() x) ->
   {within `[a, +oo[, continuous f} ->
@@ -1737,7 +1737,7 @@ apply: (@ler0_derive1_nincry _ (- f)) => //.
   exact: subset_itvr.
 Qed.
 
-Lemma le0r_derive1_ndecrNy {R : realType} (f : R -> R) (b : R) :
+Lemma ger0_derive1_ndecrNy {R : realType} (f : R -> R) (b : R) :
   (forall x, x \in `]-oo, b[%R -> derivable f x 1) ->
   (forall x, x \in `]-oo, b[%R -> 0 <= f^`() x) ->
   {within `]-oo, b], continuous f} ->