rename ge0r to ger0

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
 

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} ->