From ffe70469782dcb4796c8ad9ded1702491bd1ccc1 Mon Sep 17 00:00:00 2001
From: Alistair Sirman <alistair.sirman@gmail.com>
Date: Wed, 7 Jan 2026 16:32:19 +0000
Subject: [PATCH 01/13] Added differentiability of the max function

Added a lemma for showing \max is differentiable

Added two lemmas for differentiating the max function when the order is known at
the point.
---
 theories/derive.v | 163 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 163 insertions(+)

diff --git a/theories/derive.v b/theories/derive.v
index 18a80fa3df..c353bdce83 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -552,6 +552,7 @@ Proof. by apply/diff_unique; have [] := dcst a x. Qed.
 
 Variables (V W : normedModType R).
 
+
 Lemma differentiable_cst (W' : normedModType R) (a : W') (x : V) :
   differentiable (cst a) x.
 Proof. by apply/diff_locallyP; rewrite diff_cst; have := dcst a x. Qed.
@@ -1268,6 +1269,168 @@ Proof.
 by apply/funext => x; rewrite derive1E deriveB// derive_id derive_cst sub0r.
 Qed.
 
+Section Derive_max.
+Context {K : realType}.
+Implicit Types f g : K -> K.
+Implicit Type x : K.
+
+Lemma differentiable_max f g x (fg_neq : f x <> g x) (f_diff : differentiable f x) (g_diff : differentiable g x) :
+  differentiable (f \max g) x.
+Proof.
+case: (ltgtP (f x) (g x)) => // fg_order.
+  rewrite /Order.max_fun /maxr -derivable1_diffP /derivable fg_order.
+  have Hnear : \forall y \near nbhs 0^', (f (y%:A + x)%E < g (y%:A + x)%E)%R.
+    near=> y.
+    rewrite scaler1 -subr_lt0.
+    rewrite (_ : f (y + x) - _ = ((f - g) \o shift x) y) => //.
+    near: y.
+    apply/cvgr_lt;
+    last first.
+      move: fg_order.
+      rewrite -subr_lt0.
+      by apply.
+    apply:cvgB;
+    rewrite cvgr_dnbhsP;
+    move=> u [n_neq0 u0].
+      have Hshift : u n + x @[n --> \oo] --> x.
+        rewrite -(add0r x).
+        apply:cvgD.
+          by apply u0.
+        rewrite add0r /=.
+        by apply:cvg_cst.
+      rewrite /=.
+      apply: cvg_comp.
+        by apply Hshift.
+      move:f_diff => /differentiable_continuous.
+      by apply.
+    have Hshift : u n + x @[n --> \oo] --> x.
+      rewrite -(add0r x).
+      apply:cvgD.
+        by apply u0.
+      rewrite add0r /=.
+      by apply:cvg_cst.
+    rewrite (_ : g (u n + x)%E @[n--> \oo] = (g \o shift x) (u n) @[n --> \oo]) => //=.
+    apply: cvg_comp.
+      by apply Hshift.
+    move:g_diff => /differentiable_continuous.
+    by apply.
+  rewrite (_ : (h^-1 *: (_ - g x) @[h --> 0^']) = (fun y => y^-1 *: (shift (- g x) \o (g \o shift x)) y%:A) h @[h --> 0^']).
+    move: g_diff.
+    by rewrite -derivable1_diffP /derivable /=.
+  apply/funext => /= y.
+  apply/propext;
+  split.
+    apply: near_eq_cvg.
+    near=> z.
+    rewrite ifT //=.
+    near: z.
+    by apply Hnear.
+  apply: near_eq_cvg.
+  near=> z.
+  rewrite ifT //=.
+  near: z.
+  by apply Hnear.
+rewrite /Order.max_fun /maxr -derivable1_diffP /derivable.
+have := fg_order.
+rewrite ltNge le_eqVlt negb_or => /andP [_ fg_norder].
+rewrite ifN //.
+have Hnear : \forall y \near nbhs 0^', ~~ (f (y%:A + x)%E < g (y%:A + x)%E)%R.
+  near=> y.
+  rewrite ltNge negbK.
+  rewrite scaler1.
+  rewrite - subr_le0.
+  rewrite (_ : g (y + x) - _ = ((g - f) \o shift x) y) => //.
+  near: y.
+  apply/cvgr_le;
+  last first.
+    move: fg_order.
+    rewrite -subr_lt0.
+    by apply.
+  apply:cvgB;
+  rewrite cvgr_dnbhsP;
+  move=> u [n_neq0 u0].
+    have Hshift : u n + x @[n --> \oo] --> x.
+      rewrite -(add0r x).
+      apply:cvgD.
+        by apply u0.
+      rewrite add0r /=.
+      by apply:cvg_cst.
+    rewrite (_ : g (u n + x)%E @[n--> \oo] = (g \o shift x) (u n) @[n --> \oo]) => //=.
+    rewrite //=.
+    apply: cvg_comp.
+      by apply Hshift.
+    move:g_diff => /differentiable_continuous.
+    by apply.
+  have Hshift : u n + x @[n --> \oo] --> x.
+    rewrite -(add0r x).
+    apply:(cvgD u0).
+    rewrite add0r /=.
+    by apply:cvg_cst.
+  rewrite /=.
+  apply: cvg_comp.
+    by apply Hshift.
+  move:f_diff => /differentiable_continuous.
+  by apply.
+rewrite (_ : (h^-1 *: (_ - f x) @[h --> 0^']) = (fun y => y^-1 *: (shift (- f x) \o (f \o shift x)) y%:A) h @[h --> 0^']).
+  move: f_diff.
+  rewrite -derivable1_diffP /derivable /=.
+  by apply.
+apply/funext => /= y.
+apply/propext;
+  split.
+  apply: near_eq_cvg.
+  near=> z.
+  rewrite ifN //=.
+  near: z.
+  apply Hnear.
+apply: near_eq_cvg.
+near=> z.
+rewrite ifN //=.
+near: z.
+by apply Hnear.
+Unshelve.
+all: end_near.
+Qed.
+
+Lemma max_diffl f g x (f_gt_g : f x > g x) (f_cont : continuous_at x f) (g_cont : continuous_at x g) :
+  (f \max g)^`() x = f^`() x.
+Proof.
+rewrite !derive1E.
+apply near_eq_derive.
+  lra.
+rewrite /Order.max_fun /maxr.
+near=> y.
+rewrite ifN // -leNgt -subr_le0.
+near: y.
+apply:cvgr_le; last first.
+  rewrite -subr_lt0 in f_gt_g.
+  by apply f_gt_g.
+by apply:cvgB.
+Unshelve.
+end_near.
+Qed.
+
+Lemma max_diffr f g x (f_lt_g : f x < g x) (f_cont : continuous_at x f) (g_cont : continuous_at x g) :
+  (f \max g)^`() x = g^`() x.
+Proof.
+rewrite !derive1E.
+apply near_eq_derive=> //=.
+  lra.
+rewrite /Order.max_fun /maxr.
+near=> y.
+rewrite ifT // -subr_lt0.
+near: y.
+apply: cvgr_lt;
+    last first.
+  rewrite -subr_lt0 in f_lt_g.
+  by apply f_lt_g.
+by apply:cvgB.
+Unshelve.
+end_near.
+Qed.
+
+End Derive_max.
+
 Section Derive_lemmasVR.
 Variables (R : numFieldType) (V : normedModType R).
 Implicit Types (f g : V -> R) (x v : V).

From 10019faf3149a5e9ea86886726a903883f549007 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Mon, 26 Jan 2026 21:44:28 +0900
Subject: [PATCH 02/13] linting

---
 CHANGELOG_UNRELEASED.md |   9 ++
 classical/functions.v   |   4 +
 theories/derive.v       | 204 ++++++++--------------------------------
 3 files changed, 54 insertions(+), 163 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 68f7edf1a6..7746a73302 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -186,6 +186,15 @@
   + `closure_subset` -> `closureS`
 
 - in `set_interval.v`:
+- in `functions.v`:
+  + lemma `fun_maxC`
+
+- in `derive.v`:
+  + lemmas `differentiable_max`, `derive1_maxl`, `derive1_maxr`
+
+### Renamed
+
+- in set_interval.v
   + `itv_is_ray` -> `itv_is_open_unbounded`
   + `itv_is_bd_open` -> `itv_is_oo`
 
diff --git a/classical/functions.v b/classical/functions.v
index a8a65817de..f762c6830e 100644
--- a/classical/functions.v
+++ b/classical/functions.v
@@ -2677,6 +2677,10 @@ Lemma mul_funC (T : Type) {R : comPzSemiRingType} (f : T -> R) (r : R) :
   r \*o f = r \o* f.
 Proof. by apply/funext => x/=; rewrite mulrC. Qed.
 
+Lemma fun_maxC d d' (T : orderType d) (T' : orderType d') (f g : T -> T') :
+  f \max g = g \max f.
+Proof. by apply/funext => z/=; rewrite Order.TotalTheory.maxC. Qed.
+
 End function_space.
 
 Section function_space_lemmas.
diff --git a/theories/derive.v b/theories/derive.v
index c353bdce83..22285c0a1b 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -552,7 +552,6 @@ Proof. by apply/diff_unique; have [] := dcst a x. Qed.
 
 Variables (V W : normedModType R).
 
-
 Lemma differentiable_cst (W' : normedModType R) (a : W') (x : V) :
   differentiable (cst a) x.
 Proof. by apply/diff_locallyP; rewrite diff_cst; have := dcst a x. Qed.
@@ -1269,168 +1268,6 @@ Proof.
 by apply/funext => x; rewrite derive1E deriveB// derive_id derive_cst sub0r.
 Qed.
 
-Section Derive_max.
-Context {K : realType}.
-Implicit Types f g : K -> K.
-Implicit Type x : K.
-
-Lemma differentiable_max f g x (fg_neq : f x <> g x) (f_diff : differentiable f x) (g_diff : differentiable g x) :
-  differentiable (f \max g) x.
-Proof.
-case: (ltgtP (f x) (g x)) => // fg_order.
-  rewrite /Order.max_fun /maxr -derivable1_diffP /derivable fg_order.
-  have Hnear : \forall y \near nbhs 0^', (f (y%:A + x)%E < g (y%:A + x)%E)%R.
-    near=> y.
-    rewrite scaler1 -subr_lt0.
-    rewrite (_ : f (y + x) - _ = ((f - g) \o shift x) y) => //.
-    near: y.
-    apply/cvgr_lt;
-    last first.
-      move: fg_order.
-      rewrite -subr_lt0.
-      by apply.
-    apply:cvgB;
-    rewrite cvgr_dnbhsP;
-    move=> u [n_neq0 u0].
-      have Hshift : u n + x @[n --> \oo] --> x.
-        rewrite -(add0r x).
-        apply:cvgD.
-          by apply u0.
-        rewrite add0r /=.
-        by apply:cvg_cst.
-      rewrite /=.
-      apply: cvg_comp.
-        by apply Hshift.
-      move:f_diff => /differentiable_continuous.
-      by apply.
-    have Hshift : u n + x @[n --> \oo] --> x.
-      rewrite -(add0r x).
-      apply:cvgD.
-        by apply u0.
-      rewrite add0r /=.
-      by apply:cvg_cst.
-    rewrite (_ : g (u n + x)%E @[n--> \oo] = (g \o shift x) (u n) @[n --> \oo]) => //=.
-    apply: cvg_comp.
-      by apply Hshift.
-    move:g_diff => /differentiable_continuous.
-    by apply.
-  rewrite (_ : (h^-1 *: (_ - g x) @[h --> 0^']) = (fun y => y^-1 *: (shift (- g x) \o (g \o shift x)) y%:A) h @[h --> 0^']).
-    move: g_diff.
-    by rewrite -derivable1_diffP /derivable /=.
-  apply/funext => /= y.
-  apply/propext;
-  split.
-    apply: near_eq_cvg.
-    near=> z.
-    rewrite ifT //=.
-    near: z.
-    by apply Hnear.
-  apply: near_eq_cvg.
-  near=> z.
-  rewrite ifT //=.
-  near: z.
-  by apply Hnear.
-rewrite /Order.max_fun /maxr -derivable1_diffP /derivable.
-have := fg_order.
-rewrite ltNge le_eqVlt negb_or => /andP [_ fg_norder].
-rewrite ifN //.
-have Hnear : \forall y \near nbhs 0^', ~~ (f (y%:A + x)%E < g (y%:A + x)%E)%R.
-  near=> y.
-  rewrite ltNge negbK.
-  rewrite scaler1.
-  rewrite - subr_le0.
-  rewrite (_ : g (y + x) - _ = ((g - f) \o shift x) y) => //.
-  near: y.
-  apply/cvgr_le;
-  last first.
-    move: fg_order.
-    rewrite -subr_lt0.
-    by apply.
-  apply:cvgB;
-  rewrite cvgr_dnbhsP;
-  move=> u [n_neq0 u0].
-    have Hshift : u n + x @[n --> \oo] --> x.
-      rewrite -(add0r x).
-      apply:cvgD.
-        by apply u0.
-      rewrite add0r /=.
-      by apply:cvg_cst.
-    rewrite (_ : g (u n + x)%E @[n--> \oo] = (g \o shift x) (u n) @[n --> \oo]) => //=.
-    rewrite //=.
-    apply: cvg_comp.
-      by apply Hshift.
-    move:g_diff => /differentiable_continuous.
-    by apply.
-  have Hshift : u n + x @[n --> \oo] --> x.
-    rewrite -(add0r x).
-    apply:(cvgD u0).
-    rewrite add0r /=.
-    by apply:cvg_cst.
-  rewrite /=.
-  apply: cvg_comp.
-    by apply Hshift.
-  move:f_diff => /differentiable_continuous.
-  by apply.
-rewrite (_ : (h^-1 *: (_ - f x) @[h --> 0^']) = (fun y => y^-1 *: (shift (- f x) \o (f \o shift x)) y%:A) h @[h --> 0^']).
-  move: f_diff.
-  rewrite -derivable1_diffP /derivable /=.
-  by apply.
-apply/funext => /= y.
-apply/propext;
-  split.
-  apply: near_eq_cvg.
-  near=> z.
-  rewrite ifN //=.
-  near: z.
-  apply Hnear.
-apply: near_eq_cvg.
-near=> z.
-rewrite ifN //=.
-near: z.
-by apply Hnear.
-Unshelve.
-all: end_near.
-Qed.
-
-Lemma max_diffl f g x (f_gt_g : f x > g x) (f_cont : continuous_at x f) (g_cont : continuous_at x g) :
-  (f \max g)^`() x = f^`() x.
-Proof.
-rewrite !derive1E.
-apply near_eq_derive.
-  lra.
-rewrite /Order.max_fun /maxr.
-near=> y.
-rewrite ifN // -leNgt -subr_le0.
-near: y.
-apply:cvgr_le; last first.
-  rewrite -subr_lt0 in f_gt_g.
-  by apply f_gt_g.
-by apply:cvgB.
-Unshelve.
-end_near.
-Qed.
-
-Lemma max_diffr f g x (f_lt_g : f x < g x) (f_cont : continuous_at x f) (g_cont : continuous_at x g) :
-  (f \max g)^`() x = g^`() x.
-Proof.
-rewrite !derive1E.
-apply near_eq_derive=> //=.
-  lra.
-rewrite /Order.max_fun /maxr.
-near=> y.
-rewrite ifT // -subr_lt0.
-near: y.
-apply: cvgr_lt;
-    last first.
-  rewrite -subr_lt0 in f_lt_g.
-  by apply f_lt_g.
-by apply:cvgB.
-Unshelve.
-end_near.
-Qed.
-
-End Derive_max.
-
 Section Derive_lemmasVR.
 Variables (R : numFieldType) (V : normedModType R).
 Implicit Types (f g : V -> R) (x v : V).
@@ -2221,6 +2058,47 @@ move=> v0 fg [fav <-]; rewrite (near_eq_derive v0 fg).
 by apply: DeriveDef => //; exact: near_eq_derivable fav.
 Qed.
 
+Section derive_max.
+Context {K : realType}.
+Implicit Types (f g : K -> K) (x : K).
+
+Lemma differentiable_max f g x : f x != g x ->
+  differentiable f x -> differentiable g x -> differentiable (f \max g) x.
+Proof.
+move=> fg df dg.
+wlog: x f g df dg fg / f x < g x.
+  move=> wlg; move: fg; rewrite neq_lt => /orP[fg|gf].
+    by apply: wlg => //; rewrite lt_eqF.
+  by rewrite fun_maxC; apply: wlg => //; rewrite lt_eqF.
+move=> {}fg.
+apply/derivable1_diffP; rewrite /derivable/= /Num.max fg.
+rewrite [X in cvg X](_ : _ =
+    (fun y => y^-1 *: (shift (- g x) \o (g \o shift x)) y) h @[h --> 0^']).
+  move: dg; rewrite -derivable1_diffP /derivable.
+  by under eq_fun do rewrite scaler1.
+have Hnear : \forall y \near nbhs 0^', (f \o shift x) y < (g \o shift x) y.
+  near do rewrite -subr_lt0.
+  move: fg; rewrite -subr_lt0; apply: cvgr_lt.
+  by apply: cvgB; exact/continuous_withinNshiftx/differentiable_continuous.
+apply/funext => /= y.
+by apply/propext; split;
+  apply: near_eq_cvg; near do rewrite ifT //= scaler1//; exact: Hnear.
+Unshelve. all: by end_near. Qed.
+
+Lemma derive1_maxl f g x : f x > g x ->
+  continuous_at x f -> continuous_at x g -> (f \max g)^`() x = f^`() x.
+Proof.
+move=> fg cf cg; rewrite !derive1E; apply: near_eq_derive => //.
+near do rewrite /Order.max_fun /Num.max ifN// -leNgt -subr_le0.
+by move: fg; rewrite -subr_lt0; apply: cvgr_le; exact: cvgB.
+Unshelve. all: by end_near. Qed.
+
+Lemma derive1_maxr f g x : f x < g x ->
+  continuous_at x f -> continuous_at x g -> (f \max g)^`() x = g^`() x.
+Proof. by move=> fg cf cg; rewrite fun_maxC derive1_maxl. Qed.
+
+End derive_max.
+
 Lemma derive1N {R : realFieldType} (f : R -> R) (x : R) :
   derivable f x 1 -> (- f)^`() x = (- f^`()%classic x).
 Proof. by move=> fx; rewrite !derive1E deriveN. Qed.

From d91aec5ffac2df1cc0b58aaa56ce902f9468e02a Mon Sep 17 00:00:00 2001
From: Alistair Sirman <alistair.sirman@gmail.com>
Date: Wed, 28 Jan 2026 15:43:04 +0000
Subject: [PATCH 03/13] Added min derivable, generalised derive lemmas that
 rely on v != 0

---
 classical/functions.v |  17 ++++-
 theories/derive.v     | 165 ++++++++++++++++++++++++++++++++----------
 2 files changed, 142 insertions(+), 40 deletions(-)

diff --git a/classical/functions.v b/classical/functions.v
index f762c6830e..6e21c3f28d 100644
--- a/classical/functions.v
+++ b/classical/functions.v
@@ -2677,10 +2677,25 @@ Lemma mul_funC (T : Type) {R : comPzSemiRingType} (f : T -> R) (r : R) :
   r \*o f = r \o* f.
 Proof. by apply/funext => x/=; rewrite mulrC. Qed.
 
-Lemma fun_maxC d d' (T : orderType d) (T' : orderType d') (f g : T -> T') :
+Lemma min_fun_to_max (T : Type) (T' : numDomainType) (f g : T -> T') :
+  (f \min g) = (f + g) - (f \max g).
+Proof.
+apply/funext=> x /=; by rewrite minr_to_max. Qed.
+
+Lemma max_fun_to_min (T : Type) (T' : numDomainType) (f g : T -> T') :
+  (f \max g) = (f + g) - (f \min g).
+Proof.
+apply/funext => x /=; by rewrite maxr_to_min. Qed.
+
+Lemma fun_maxC d (T : Type) (T' : orderType d) (f g : T -> T') :
   f \max g = g \max f.
 Proof. by apply/funext => z/=; rewrite Order.TotalTheory.maxC. Qed.
 
+Lemma fun_minC d (T : Type) (T' : orderType d) (f g : T -> T') :
+  f \min g = g \min f.
+Proof. by apply/funext => z/=; rewrite Order.TotalTheory.minC. Qed.
+
+
 End function_space.
 
 Section function_space_lemmas.
diff --git a/theories/derive.v b/theories/derive.v
index 22285c0a1b..6986ef3673 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -304,6 +304,28 @@ move=> df; apply/derivable_nbhsP; apply/eqaddoE; rewrite funeqE => h.
 by rewrite /= addrC df.
 Qed.
 
+Lemma derivable0 (f : V -> W) (x : V) : derivable f x 0.
+Proof.
+apply:is_cvg_near_cst => //=.
+near=>h.
+by rewrite scaler0 add0r subrr scaler0.
+Unshelve.
+end_near.
+Qed.
+
+Lemma derive0 (f : V -> W) (x : V) : 'D_0 f x = 0.
+Proof.
+apply/lim_near_cst => //=.
+near=> h.
+by rewrite scaler0 add0r subrr scaler0.
+Unshelve.
+end_near.
+Qed.
+
+
+Lemma is_derive0 (f : V -> W) (x : V) : is_derive x 0 f 0.
+Proof. split; [by apply/derivable0 | by rewrite derive0]. Qed.
+
 End DifferentialR.
 
 Notation "''D_' v f" := (derive f ^~ v).
@@ -2024,80 +2046,145 @@ by rewrite [LHS]linearZ mulrC.
 Qed.
 
 Lemma near_eq_growth_rate (R : numFieldType) (V W : normedModType R)
-    (f g : V -> W) (a v : V) : v != 0 -> {near a, f =1 g} ->
+    (f g : V -> W) (a v : V) : {near a, f =1 g} ->
    \forall h \near 0,
      h^-1 *: (f (h *: v + a) - f a) = h^-1 *: (g (h *: v + a) - g a).
 Proof.
-move=> v0 fg; near do rewrite (nbhs_singleton fg) (near fg)// addrC.
+move=> fg; near do rewrite (nbhs_singleton fg) (near fg)// addrC.
 apply/(@near0Z _ _ _ [set v | (a + v) \is_near (nbhs a)])=> /=.
 by rewrite (near_shift a)/=; near do rewrite /= sub0r addrC addrNK//.
 Unshelve. all: by end_near. Qed.
 
 Lemma near_eq_derivable (R : numFieldType) (V W : normedModType R)
-    (f g : V -> W) (a v : V) : v != 0 ->
+    (f g : V -> W) (a v : V) :
   {near a, f =1 g} -> derivable f a v -> derivable g a v.
 Proof.
+case: (eqVneq v 0)=> [-> _ _| ].
+by apply/derivable0.
 move=> vn0 nfg /cvg_ex[/= l fl]; apply/cvg_ex; exists l => /=.
 exact/(cvg_trans _ fl)/near_eq_cvg/cvg_within/near_eq_growth_rate.
 Qed.
 
 Lemma near_eq_derive (R : numFieldType) (V W : normedModType R)
   (f g : V -> W) (a v : V) :
-  v != 0 -> (\near a, f a = g a) -> 'D_v f a = 'D_v g a.
+  (\near a, f a = g a) -> 'D_v f a = 'D_v g a.
 Proof.
+case: (eqVneq v 0)=> [-> _ | ].
+by rewrite !derive0.
 move=> v0 fg; rewrite /derive; congr (lim _).
 rewrite eqEsubset; split; apply/near_eq_cvg/cvg_within/near_eq_growth_rate => //.
 by near do apply/esym.
 Unshelve. all: by end_near. Qed.
 
 Lemma near_eq_is_derive (R : numFieldType) (V W : normedModType R)
-    (f g : V -> W) (a v : V) (df : W) : v != 0 ->
+    (f g : V -> W) (a v : V) (df : W) :
   (\near a, f a = g a) -> is_derive a v f df -> is_derive a v g df.
 Proof.
-move=> v0 fg [fav <-]; rewrite (near_eq_derive v0 fg).
+move=> fg [fav <-]; rewrite (near_eq_derive _ fg).
 by apply: DeriveDef => //; exact: near_eq_derivable fav.
 Qed.
 
-Section derive_max.
-Context {K : realType}.
-Implicit Types (f g : K -> K) (x : K).
-
-Lemma differentiable_max f g x : f x != g x ->
-  differentiable f x -> differentiable g x -> differentiable (f \max g) x.
-Proof.
-move=> fg df dg.
-wlog: x f g df dg fg / f x < g x.
-  move=> wlg; move: fg; rewrite neq_lt => /orP[fg|gf].
-    by apply: wlg => //; rewrite lt_eqF.
-  by rewrite fun_maxC; apply: wlg => //; rewrite lt_eqF.
-move=> {}fg.
-apply/derivable1_diffP; rewrite /derivable/= /Num.max fg.
-rewrite [X in cvg X](_ : _ =
-    (fun y => y^-1 *: (shift (- g x) \o (g \o shift x)) y) h @[h --> 0^']).
-  move: dg; rewrite -derivable1_diffP /derivable.
-  by under eq_fun do rewrite scaler1.
-have Hnear : \forall y \near nbhs 0^', (f \o shift x) y < (g \o shift x) y.
-  near do rewrite -subr_lt0.
-  move: fg; rewrite -subr_lt0; apply: cvgr_lt.
-  by apply: cvgB; exact/continuous_withinNshiftx/differentiable_continuous.
-apply/funext => /= y.
-by apply/propext; split;
-  apply: near_eq_cvg; near do rewrite ifT //= scaler1//; exact: Hnear.
+Section Derive_max.
+Context {K : realType} {V W : normedModType K}.
+Implicit Types f g : V -> K^o.
+Implicit Type x : V.
+
+Fact der_max f g x v :
+  f x <> g x -> derivable f x v -> derivable g x v ->
+  {for x, continuous f} -> {for x, continuous g} ->
+  (fun h => h^-1 *: (((f \max g) \o shift x) (h *: v) - (f \max g) x)) @
+    0^' --> if f x < g x then 'D_v g x else 'D_v f x.
+Proof.
+wlog: f g x / f x < g x.
+  move=> wlg fx_neq_gx.
+  move: (fx_neq_gx) => /eqP.
+  rewrite neq_lt => /orP[fg|gf].
+    move: fg fx_neq_gx.
+    by apply:wlg.
+  move=> df dg cf cg.
+  move: dg df cg cf.
+  rewrite fun_maxC ltNge if_neg le_eqVlt.
+  move: fx_neq_gx => /nesym/[dup] fx_neq_gx /eqP/negPf -> /=.
+  by apply:(wlg g f).
+move=> fx_lt_gx fg_neq df dg cf cg.
+case: ifPn => fg /=.
+  rewrite /Num.max fg => t Ht.
+  apply:(@near_eq_cvg _ _ _ _ (fun h => h^-1 *: (g (h *: v + x) - g x))).
+    near=> h.
+    rewrite ifT // -subr_lt0 (_ : f _ - _ = ((f - g) \o shift x) (h *: v)) //.
+    near: h.
+    have Hf : forall f : V -> K^o,
+    continuous_at x f -> f (shift x (x0 *: v)) @[x0 --> nbhs 0^'] --> f x.
+      move=> f' cf'.
+      apply:cvg_comp; last by apply:cf'.
+      rewrite -[in nbhs x](add0r x).
+      apply:cvgD; last by apply:cvg_cst.
+      rewrite -(scale0r v).
+      apply:cvgZ; last by apply:cvg_cst.
+      by apply:nbhs_dnbhs.
+    apply/cvgr_lt; last by move: fg; rewrite -subr_lt0; apply.
+    by apply:cvgB; apply:Hf.
+  by apply:dg.
+exfalso.
+by apply: (negP fg).
+Unshelve.
+end_near.
+Qed.
+
+Lemma derivable_max f g x v :
+  f x <> g x -> derivable f x v -> derivable g x v ->
+  {for x, continuous f} -> {for x, continuous g} ->
+  derivable (f \max g) x v.
+Proof.
+move=> fx_gx df dg cf cg; apply/cvg_ex.
+exists(if f x < g x then 'D_v g x else 'D_v f x).
+exact: der_max.
+Qed.
+
+Lemma derive_maxl f g x v : f x > g x ->
+  {for x, continuous f} -> {for x, continuous g} ->
+  'D_v (f \max g) x = 'D_v f x.
+Proof.
+case: (boolP (v == 0)) => [/eqP -> //= gx_fx cf cg | v0].
+  by rewrite !derive0.
+move=> fg cf cg; apply: near_eq_derive => //.
+near do rewrite /Order.max_fun /Num.max ifN// -leNgt -subr_le0.
+by move: fg; rewrite -subr_lt0; apply: cvgr_le; exact: cvgB.
 Unshelve. all: by end_near. Qed.
 
-Lemma derive1_maxl f g x : f x > g x ->
-  continuous_at x f -> continuous_at x g -> (f \max g)^`() x = f^`() x.
+Lemma derive_maxr f g x v : f x < g x ->
+  {for x, continuous f} -> {for x, continuous g} ->
+  'D_v (f \max g) x = 'D_v g x.
+Proof. by move=> fg cf cg; rewrite fun_maxC derive_maxl. Qed.
+
+Lemma derivable_min f g x v :
+  f x <> g x -> derivable f x v -> derivable g x v ->
+  {for x, continuous f} -> {for x, continuous g} ->
+  derivable (f \min g) x v.
 Proof.
-move=> fg cf cg; rewrite !derive1E; apply: near_eq_derive => //.
-near do rewrite /Order.max_fun /Num.max ifN// -leNgt -subr_le0.
+case: (boolP (v == 0)) => [/eqP -> /= gx_fx cf cg | v0].
+  by rewrite !derive0.
+rewrite min_fun_to_max=> fx_gx df dg cf cg.
+apply/derivableB; [by apply/(derivableD df dg) | by apply/derivable_max].
+Qed.
+
+Lemma derive_minr f g x v : f x > g x ->
+  {for x, continuous f} -> {for x, continuous g} ->
+  'D_v (f \min g) x = 'D_v g x.
+Proof.
+case: (boolP (v == 0)) => [/eqP -> //= gx_fx cf cg | v0].
+  by rewrite !derive0.
+move=> fg cf cg; apply: near_eq_derive => //.
+near do rewrite /Order.min_fun /Num.min ifN// -leNgt -subr_le0.
 by move: fg; rewrite -subr_lt0; apply: cvgr_le; exact: cvgB.
 Unshelve. all: by end_near. Qed.
 
-Lemma derive1_maxr f g x : f x < g x ->
-  continuous_at x f -> continuous_at x g -> (f \max g)^`() x = g^`() x.
-Proof. by move=> fg cf cg; rewrite fun_maxC derive1_maxl. Qed.
+Lemma derive_minl f g x v : f x < g x ->
+  {for x, continuous f} -> {for x, continuous g} ->
+  'D_v (f \min g) x = 'D_v f x.
+Proof. by move=> fg cf cg; rewrite fun_minC derive_minr. Qed.
 
-End derive_max.
+End Derive_max.
 
 Lemma derive1N {R : realFieldType} (f : R -> R) (x : R) :
   derivable f x 1 -> (- f)^`() x = (- f^`()%classic x).

From 64910a15023ad294f717cc4b9b49ee5fca2b3139 Mon Sep 17 00:00:00 2001
From: Alistair Sirman <alistair.sirman@gmail.com>
Date: Fri, 23 Jan 2026 11:29:36 +0000
Subject: [PATCH 04/13] Added lemma to swap mathcomp natural log with Rocqs
 natural log

---
 CHANGELOG_UNRELEASED.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 7746a73302..f5671417cc 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -10,6 +10,11 @@
   + lemma `itv_closed_ends_closed`
 - in `classical_sets.v`
   + lemma `in_set1_eq`
+- in `analysis_stdlib/Rstruct_topology.v`:
+  + lemma `RlnE`
+
+- in `classical_sets.v`:
+  + lemma `nonemptyPn`
 
 - in `set_interval.v`
   + definitions `itv_is_closed_unbounded`, `itv_is_cc`, `itv_closed_ends`

From 33034fe6fb07d6376eab3ec0d0fea2547b7e5dba Mon Sep 17 00:00:00 2001
From: Alistair Sirman <alistair.sirman@gmail.com>
Date: Wed, 28 Jan 2026 15:54:53 +0000
Subject: [PATCH 05/13] Revert "Merge branch 'ln_eq_Rln' into HEAD"

This reverts commit 6be770c8b813c51e936a444916c4e7c721ef749f, reversing
changes made to 6d24c456db2f6239680d170abe9a8d1718616ee1.
---
 CHANGELOG_UNRELEASED.md            | 1 +
 analysis_stdlib/Rstruct_topology.v | 2 --
 2 files changed, 1 insertion(+), 2 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index f5671417cc..ed2a3de89c 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -17,6 +17,7 @@
   + lemma `nonemptyPn`
 
 - in `set_interval.v`
+- in set_interval.v
   + definitions `itv_is_closed_unbounded`, `itv_is_cc`, `itv_closed_ends`
 
 - in `Rstruct.v`:
diff --git a/analysis_stdlib/Rstruct_topology.v b/analysis_stdlib/Rstruct_topology.v
index 330d17b638..ed284aa841 100644
--- a/analysis_stdlib/Rstruct_topology.v
+++ b/analysis_stdlib/Rstruct_topology.v
@@ -14,8 +14,6 @@ From mathcomp Require Export Rstruct.
 From mathcomp Require Import topology.
 (* The following line is for RexpE. *)
 From mathcomp Require normedtype sequences.
-(* The following line is for RlnE. *)
-From mathcomp Require exp.
 
 Set Implicit Arguments.
 Unset Strict Implicit.

From d88deeba5275b2ed703179278f485847bb90f506 Mon Sep 17 00:00:00 2001
From: Alistair Sirman <alistair.sirman@gmail.com>
Date: Wed, 28 Jan 2026 15:57:43 +0000
Subject: [PATCH 06/13] Updated changelog

---
 CHANGELOG_UNRELEASED.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index ed2a3de89c..3e7367e806 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -193,10 +193,10 @@
 
 - in `set_interval.v`:
 - in `functions.v`:
-  + lemma `fun_maxC`
+  + lemmas `fun_maxC`, `fun_minC`, `min_fun_to_max`, `max_fun_to_min`
 
 - in `derive.v`:
-  + lemmas `differentiable_max`, `derive1_maxl`, `derive1_maxr`
+  + lemmas `derivable_max`, `derive_maxl`, `derive_maxr` `derivable_min`, `derive_minl`, `derive_minr`
 
 ### Renamed
 

From a7625aba7fc6b0e92bc2f580558718ce0cab0138 Mon Sep 17 00:00:00 2001
From: Alistair Sirman <alistair.sirman@gmail.com>
Date: Wed, 28 Jan 2026 15:59:37 +0000
Subject: [PATCH 07/13] Fixed erroneous paces

---
 CHANGELOG_UNRELEASED.md | 1 -
 classical/functions.v   | 1 -
 theories/derive.v       | 1 -
 3 files changed, 3 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 3e7367e806..fa84a0bb40 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -199,7 +199,6 @@
   + lemmas `derivable_max`, `derive_maxl`, `derive_maxr` `derivable_min`, `derive_minl`, `derive_minr`
 
 ### Renamed
-
 - in set_interval.v
   + `itv_is_ray` -> `itv_is_open_unbounded`
   + `itv_is_bd_open` -> `itv_is_oo`
diff --git a/classical/functions.v b/classical/functions.v
index 6e21c3f28d..3913b547ca 100644
--- a/classical/functions.v
+++ b/classical/functions.v
@@ -2695,7 +2695,6 @@ Lemma fun_minC d (T : Type) (T' : orderType d) (f g : T -> T') :
   f \min g = g \min f.
 Proof. by apply/funext => z/=; rewrite Order.TotalTheory.minC. Qed.
 
-
 End function_space.
 
 Section function_space_lemmas.
diff --git a/theories/derive.v b/theories/derive.v
index 6986ef3673..74b911b3e1 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -322,7 +322,6 @@ Unshelve.
 end_near.
 Qed.
 
-
 Lemma is_derive0 (f : V -> W) (x : V) : is_derive x 0 f 0.
 Proof. split; [by apply/derivable0 | by rewrite derive0]. Qed.
 

From cea8b3db9d06be4615786b57b12eb936ce5370a6 Mon Sep 17 00:00:00 2001
From: Alistair Sirman <alistair.sirman@gmail.com>
Date: Wed, 28 Jan 2026 16:10:44 +0000
Subject: [PATCH 08/13] Fixed issue finding lemma

---
 classical/functions.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/classical/functions.v b/classical/functions.v
index 3913b547ca..0da21a0479 100644
--- a/classical/functions.v
+++ b/classical/functions.v
@@ -2680,12 +2680,12 @@ Proof. by apply/funext => x/=; rewrite mulrC. Qed.
 Lemma min_fun_to_max (T : Type) (T' : numDomainType) (f g : T -> T') :
   (f \min g) = (f + g) - (f \max g).
 Proof.
-apply/funext=> x /=; by rewrite minr_to_max. Qed.
+apply/funext=> x /=; by rewrite Num.Theory.minr_to_max. Qed.
 
 Lemma max_fun_to_min (T : Type) (T' : numDomainType) (f g : T -> T') :
   (f \max g) = (f + g) - (f \min g).
 Proof.
-apply/funext => x /=; by rewrite maxr_to_min. Qed.
+apply/funext => x /=; by rewrite Num.Theory.maxr_to_min. Qed.
 
 Lemma fun_maxC d (T : Type) (T' : orderType d) (f g : T -> T') :
   f \max g = g \max f.

From 565d317431285bcd3ddc0a72480a033721bd0b04 Mon Sep 17 00:00:00 2001
From: Alistair Sirman <alistair.sirman@gmail.com>
Date: Wed, 28 Jan 2026 17:19:33 +0000
Subject: [PATCH 09/13] Fixed error

---
 theories/derive.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/derive.v b/theories/derive.v
index 74b911b3e1..6f00f78dbc 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -2161,8 +2161,8 @@ Lemma derivable_min f g x v :
   {for x, continuous f} -> {for x, continuous g} ->
   derivable (f \min g) x v.
 Proof.
-case: (boolP (v == 0)) => [/eqP -> /= gx_fx cf cg | v0].
-  by rewrite !derive0.
+case: (boolP (v == 0)) => [/eqP -> /= _ _ _ _ _| v0].
+  by apply/derivable0.
 rewrite min_fun_to_max=> fx_gx df dg cf cg.
 apply/derivableB; [by apply/(derivableD df dg) | by apply/derivable_max].
 Qed.

From d219a5c07d5861a8811c41a8c1512064db246833 Mon Sep 17 00:00:00 2001
From: Alistair Sirman <alistair.sirman@gmail.com>
Date: Wed, 28 Jan 2026 17:51:32 +0000
Subject: [PATCH 10/13] Removed dependence on direction that's no longer needed

---
 theories/exp.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/theories/exp.v b/theories/exp.v
index 84e14e84ab..f0d409c538 100644
--- a/theories/exp.v
+++ b/theories/exp.v
@@ -1088,9 +1088,11 @@ apply: (@cvg_comp _ _ _ _ _ _ (@ninfty_nbhs R)).
 exact/cvgNy_compNP/cvgr_expR.
 Unshelve. end_near. Qed.
 
-Lemma derivable_powR v x : v != 0 ->
+Lemma derivable_powR v x :
   {in `]0, +oo[, forall a, derivable (powR ^~ x) a v}.
 Proof.
+case: (eqVneq v 0)=> [-> y _| ].
+by apply/derivable0.
 move=> v0 a; rewrite in_itv/= andbT => a0.
 apply: (@near_eq_derivable _ _ _ (fun a' => expR (x * ln a'))) => //.
   by near=> b; rewrite /powR gt_eqF//; near: b; exact: lt_nbhsr.

From 98d8d73b3b2ec261e3c6cc72d2b44b15faff4696 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Sat, 28 Feb 2026 00:37:19 +0900
Subject: [PATCH 11/13] linting

---
 CHANGELOG_UNRELEASED.md |   4 ++
 classical/functions.v   |  10 ++--
 theories/derive.v       | 112 +++++++++++++++++-----------------------
 3 files changed, 54 insertions(+), 72 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index fa84a0bb40..367bd99c54 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -197,6 +197,7 @@
 
 - in `derive.v`:
   + lemmas `derivable_max`, `derive_maxl`, `derive_maxr` `derivable_min`, `derive_minl`, `derive_minr`
+  + lemmas `derivable0`, `derive0`, `is_derive0`
 
 ### Renamed
 - in set_interval.v
@@ -237,6 +238,9 @@
 - in `lebesgue_integral_nonneg.v`:
   + lemmas `integral_itv_bndo_bndc`, `integral_itv_obnd_cbnd`,
     `integral_itv_bndoo`
+- in `derive.v`:
+  + lemmas `near_eq_growth_rate`, `near_eq_derivable`, `near_eq_derive`,
+    `near_eq_is_derive`
 
 ### Deprecated
 
diff --git a/classical/functions.v b/classical/functions.v
index 0da21a0479..1021fba49d 100644
--- a/classical/functions.v
+++ b/classical/functions.v
@@ -2679,19 +2679,17 @@ Proof. by apply/funext => x/=; rewrite mulrC. Qed.
 
 Lemma min_fun_to_max (T : Type) (T' : numDomainType) (f g : T -> T') :
   (f \min g) = (f + g) - (f \max g).
-Proof.
-apply/funext=> x /=; by rewrite Num.Theory.minr_to_max. Qed.
+Proof. by apply/funext=> x/=; rewrite Num.Theory.minr_to_max. Qed.
 
 Lemma max_fun_to_min (T : Type) (T' : numDomainType) (f g : T -> T') :
   (f \max g) = (f + g) - (f \min g).
-Proof.
-apply/funext => x /=; by rewrite Num.Theory.maxr_to_min. Qed.
+Proof. by apply/funext => x/=; rewrite Num.Theory.maxr_to_min. Qed.
 
-Lemma fun_maxC d (T : Type) (T' : orderType d) (f g : T -> T') :
+Lemma fun_maxC (T : Type) d (T' : orderType d) (f g : T -> T') :
   f \max g = g \max f.
 Proof. by apply/funext => z/=; rewrite Order.TotalTheory.maxC. Qed.
 
-Lemma fun_minC d (T : Type) (T' : orderType d) (f g : T -> T') :
+Lemma fun_minC (T : Type) d (T' : orderType d) (f g : T -> T') :
   f \min g = g \min f.
 Proof. by apply/funext => z/=; rewrite Order.TotalTheory.minC. Qed.
 
diff --git a/theories/derive.v b/theories/derive.v
index 6f00f78dbc..3fd1a338e8 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -4,8 +4,8 @@ From mathcomp Require Import all_ssreflect_compat ssralg ssrnum matrix interval
 From mathcomp Require Import sesquilinear.
 #[warning="-warn-library-file-internal-analysis"]
 From mathcomp Require Import unstable.
-From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
-From mathcomp Require Import reals interval_inference topology.
+From mathcomp Require Import mathcomp_extra boolp contra classical_sets.
+From mathcomp Require Import functions reals interval_inference topology.
 From mathcomp Require Import prodnormedzmodule tvs normedtype landau.
 
 (**md**************************************************************************)
@@ -306,24 +306,20 @@ Qed.
 
 Lemma derivable0 (f : V -> W) (x : V) : derivable f x 0.
 Proof.
-apply:is_cvg_near_cst => //=.
-near=>h.
+apply: (is_cvg_near_cst 0) => //=.
+near=> h.
 by rewrite scaler0 add0r subrr scaler0.
-Unshelve.
-end_near.
-Qed.
+Unshelve. all: by end_near. Qed.
 
 Lemma derive0 (f : V -> W) (x : V) : 'D_0 f x = 0.
 Proof.
 apply/lim_near_cst => //=.
 near=> h.
 by rewrite scaler0 add0r subrr scaler0.
-Unshelve.
-end_near.
-Qed.
+Unshelve. all: by end_near. Qed.
 
 Lemma is_derive0 (f : V -> W) (x : V) : is_derive x 0 f 0.
-Proof. split; [by apply/derivable0 | by rewrite derive0]. Qed.
+Proof. by split; [exact/derivable0|rewrite derive0]. Qed.
 
 End DifferentialR.
 
@@ -2058,8 +2054,7 @@ Lemma near_eq_derivable (R : numFieldType) (V W : normedModType R)
     (f g : V -> W) (a v : V) :
   {near a, f =1 g} -> derivable f a v -> derivable g a v.
 Proof.
-case: (eqVneq v 0)=> [-> _ _| ].
-by apply/derivable0.
+have [-> _ _|] := eqVneq v 0; first exact/derivable0.
 move=> vn0 nfg /cvg_ex[/= l fl]; apply/cvg_ex; exists l => /=.
 exact/(cvg_trans _ fl)/near_eq_cvg/cvg_within/near_eq_growth_rate.
 Qed.
@@ -2068,10 +2063,9 @@ Lemma near_eq_derive (R : numFieldType) (V W : normedModType R)
   (f g : V -> W) (a v : V) :
   (\near a, f a = g a) -> 'D_v f a = 'D_v g a.
 Proof.
-case: (eqVneq v 0)=> [-> _ | ].
-by rewrite !derive0.
+have [-> _|] := eqVneq v 0; first by rewrite !derive0.
 move=> v0 fg; rewrite /derive; congr (lim _).
-rewrite eqEsubset; split; apply/near_eq_cvg/cvg_within/near_eq_growth_rate => //.
+rewrite eqEsubset; split; apply/near_eq_cvg/cvg_within/near_eq_growth_rate =>//.
 by near do apply/esym.
 Unshelve. all: by end_near. Qed.
 
@@ -2088,55 +2082,43 @@ Context {K : realType} {V W : normedModType K}.
 Implicit Types f g : V -> K^o.
 Implicit Type x : V.
 
-Fact der_max f g x v :
-  f x <> g x -> derivable f x v -> derivable g x v ->
+Fact der_max f g x v : f x != g x ->
+  derivable f x v -> derivable g x v ->
   {for x, continuous f} -> {for x, continuous g} ->
-  (fun h => h^-1 *: (((f \max g) \o shift x) (h *: v) - (f \max g) x)) @
-    0^' --> if f x < g x then 'D_v g x else 'D_v f x.
+  (fun h => h^-1 *: (((f \max g) \o shift x) (h *: v) - (f \max g) x))
+    @ 0^' --> if f x < g x then 'D_v g x else 'D_v f x.
 Proof.
 wlog: f g x / f x < g x.
-  move=> wlg fx_neq_gx.
-  move: (fx_neq_gx) => /eqP.
-  rewrite neq_lt => /orP[fg|gf].
-    move: fg fx_neq_gx.
-    by apply:wlg.
-  move=> df dg cf cg.
-  move: dg df cg cf.
-  rewrite fun_maxC ltNge if_neg le_eqVlt.
-  move: fx_neq_gx => /nesym/[dup] fx_neq_gx /eqP/negPf -> /=.
-  by apply:(wlg g f).
-move=> fx_lt_gx fg_neq df dg cf cg.
-case: ifPn => fg /=.
-  rewrite /Num.max fg => t Ht.
-  apply:(@near_eq_cvg _ _ _ _ (fun h => h^-1 *: (g (h *: v + x) - g x))).
-    near=> h.
-    rewrite ifT // -subr_lt0 (_ : f _ - _ = ((f - g) \o shift x) (h *: v)) //.
-    near: h.
-    have Hf : forall f : V -> K^o,
-    continuous_at x f -> f (shift x (x0 *: v)) @[x0 --> nbhs 0^'] --> f x.
-      move=> f' cf'.
-      apply:cvg_comp; last by apply:cf'.
+  move=> wlg; rewrite neq_lt => /orP[fg|gf df dg fxv gxv].
+  - by apply: wlg => //; rewrite lt_eqF.
+  - rewrite fun_maxC ltNge if_neg le_eqVlt eq_sym gt_eqF//=.
+    by apply: wlg => //; rewrite lt_eqF.
+move=> fx_lt_gx fg_neq df dg cf cg; case: ifPn => fg /=.
+- rewrite /Num.max fg => A DgxA.
+  apply: (@near_eq_cvg _ _ _ _ (fun h => h^-1 *: (g (h *: v + x) - g x))).
+  + near do rewrite ifT// -subr_lt0 -[ltLHS]/(((f - g) \o shift x) (_ *: v)).
+    have Hf (h : V -> K^o) : continuous_at x h ->
+        h (shift x (k *: v)) @[k --> nbhs 0^'] --> h x.
+      move=> ch.
+      apply: cvg_comp; last exact: ch.
       rewrite -[in nbhs x](add0r x).
-      apply:cvgD; last by apply:cvg_cst.
-      rewrite -(scale0r v).
-      apply:cvgZ; last by apply:cvg_cst.
-      by apply:nbhs_dnbhs.
-    apply/cvgr_lt; last by move: fg; rewrite -subr_lt0; apply.
-    by apply:cvgB; apply:Hf.
-  by apply:dg.
-exfalso.
-by apply: (negP fg).
-Unshelve.
-end_near.
-Qed.
+      apply: cvgD; last exact: cvg_cst.
+      rewrite -(scale0r v); apply: cvgZ; last exact: cvg_cst.
+      exact: nbhs_dnbhs.
+    apply/(cvgr_lt (f x - g x)); last by rewrite subr_lt0.
+    by apply: cvgB; exact: Hf.
+  + exact: dg.
+- absurd.
+  by rewrite fx_lt_gx in fg.
+Unshelve. all: by end_near. Qed.
 
 Lemma derivable_max f g x v :
-  f x <> g x -> derivable f x v -> derivable g x v ->
+  f x != g x -> derivable f x v -> derivable g x v ->
   {for x, continuous f} -> {for x, continuous g} ->
   derivable (f \max g) x v.
 Proof.
-move=> fx_gx df dg cf cg; apply/cvg_ex.
-exists(if f x < g x then 'D_v g x else 'D_v f x).
+move=> fx_gx df dg cf cg; apply/cvg_ex => /=.
+exists (if f x < g x then 'D_v g x else 'D_v f x).
 exact: der_max.
 Qed.
 
@@ -2144,9 +2126,9 @@ Lemma derive_maxl f g x v : f x > g x ->
   {for x, continuous f} -> {for x, continuous g} ->
   'D_v (f \max g) x = 'D_v f x.
 Proof.
-case: (boolP (v == 0)) => [/eqP -> //= gx_fx cf cg | v0].
+have [-> gx_fx cf cg|v0 fg cf cg]:= eqVneq v 0.
   by rewrite !derive0.
-move=> fg cf cg; apply: near_eq_derive => //.
+apply: near_eq_derive => //.
 near do rewrite /Order.max_fun /Num.max ifN// -leNgt -subr_le0.
 by move: fg; rewrite -subr_lt0; apply: cvgr_le; exact: cvgB.
 Unshelve. all: by end_near. Qed.
@@ -2157,23 +2139,21 @@ Lemma derive_maxr f g x v : f x < g x ->
 Proof. by move=> fg cf cg; rewrite fun_maxC derive_maxl. Qed.
 
 Lemma derivable_min f g x v :
-  f x <> g x -> derivable f x v -> derivable g x v ->
+  f x != g x -> derivable f x v -> derivable g x v ->
   {for x, continuous f} -> {for x, continuous g} ->
   derivable (f \min g) x v.
 Proof.
-case: (boolP (v == 0)) => [/eqP -> /= _ _ _ _ _| v0].
-  by apply/derivable0.
-rewrite min_fun_to_max=> fx_gx df dg cf cg.
-apply/derivableB; [by apply/(derivableD df dg) | by apply/derivable_max].
+have [-> *|x0] := eqVneq v 0; first exact/derivable0.
+rewrite min_fun_to_max => fx_gx df dg cf cg.
+by apply/derivableB; [apply/(derivableD df dg) |apply/derivable_max].
 Qed.
 
 Lemma derive_minr f g x v : f x > g x ->
   {for x, continuous f} -> {for x, continuous g} ->
   'D_v (f \min g) x = 'D_v g x.
 Proof.
-case: (boolP (v == 0)) => [/eqP -> //= gx_fx cf cg | v0].
-  by rewrite !derive0.
-move=> fg cf cg; apply: near_eq_derive => //.
+have [-> *|v0 fg cf cg] := eqVneq v 0; first by rewrite !derive0.
+apply: near_eq_derive => //.
 near do rewrite /Order.min_fun /Num.min ifN// -leNgt -subr_le0.
 by move: fg; rewrite -subr_lt0; apply: cvgr_le; exact: cvgB.
 Unshelve. all: by end_near. Qed.

From c037e540b91307614faa90b8b39d795dfcf88bf6 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Sat, 28 Feb 2026 00:50:19 +0900
Subject: [PATCH 12/13] fix changelog

---
 CHANGELOG_UNRELEASED.md            | 23 ++++++++---------------
 analysis_stdlib/Rstruct_topology.v |  2 ++
 2 files changed, 10 insertions(+), 15 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 367bd99c54..45709d3d1f 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -10,14 +10,8 @@
   + lemma `itv_closed_ends_closed`
 - in `classical_sets.v`
   + lemma `in_set1_eq`
-- in `analysis_stdlib/Rstruct_topology.v`:
-  + lemma `RlnE`
-
-- in `classical_sets.v`:
-  + lemma `nonemptyPn`
 
 - in `set_interval.v`
-- in set_interval.v
   + definitions `itv_is_closed_unbounded`, `itv_is_cc`, `itv_closed_ends`
 
 - in `Rstruct.v`:
@@ -65,6 +59,13 @@
 - in `normed_module.v`:
   + lemma `within_continuous_compN`
 
+- in `functions.v`:
+  + lemmas `fun_maxC`, `fun_minC`, `min_fun_to_max`, `max_fun_to_min`
+
+- in `derive.v`:
+  + lemmas `derivable_max`, `derive_maxl`, `derive_maxr` `derivable_min`, `derive_minl`, `derive_minr`
+  + lemmas `derivable0`, `derive0`, `is_derive0`
+
 ### Changed
 - in `set_interval.v`
   + `itv_is_closed_unbounded` (fix the definition)
@@ -192,15 +193,6 @@
   + `closure_subset` -> `closureS`
 
 - in `set_interval.v`:
-- in `functions.v`:
-  + lemmas `fun_maxC`, `fun_minC`, `min_fun_to_max`, `max_fun_to_min`
-
-- in `derive.v`:
-  + lemmas `derivable_max`, `derive_maxl`, `derive_maxr` `derivable_min`, `derive_minl`, `derive_minr`
-  + lemmas `derivable0`, `derive0`, `is_derive0`
-
-### Renamed
-- in set_interval.v
   + `itv_is_ray` -> `itv_is_open_unbounded`
   + `itv_is_bd_open` -> `itv_is_oo`
 
@@ -238,6 +230,7 @@
 - in `lebesgue_integral_nonneg.v`:
   + lemmas `integral_itv_bndo_bndc`, `integral_itv_obnd_cbnd`,
     `integral_itv_bndoo`
+
 - in `derive.v`:
   + lemmas `near_eq_growth_rate`, `near_eq_derivable`, `near_eq_derive`,
     `near_eq_is_derive`
diff --git a/analysis_stdlib/Rstruct_topology.v b/analysis_stdlib/Rstruct_topology.v
index ed284aa841..330d17b638 100644
--- a/analysis_stdlib/Rstruct_topology.v
+++ b/analysis_stdlib/Rstruct_topology.v
@@ -14,6 +14,8 @@ From mathcomp Require Export Rstruct.
 From mathcomp Require Import topology.
 (* The following line is for RexpE. *)
 From mathcomp Require normedtype sequences.
+(* The following line is for RlnE. *)
+From mathcomp Require exp.
 
 Set Implicit Arguments.
 Unset Strict Implicit.

From c1543529dc582d1b779be7531d292d4fb04d5ec3 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Sat, 28 Feb 2026 01:01:37 +0900
Subject: [PATCH 13/13] fix

---
 CHANGELOG_UNRELEASED.md | 5 ++++-
 theories/exp.v          | 6 ++----
 2 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 45709d3d1f..dee7998598 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -233,7 +233,10 @@
 
 - in `derive.v`:
   + lemmas `near_eq_growth_rate`, `near_eq_derivable`, `near_eq_derive`,
-    `near_eq_is_derive`
+    `near_eq_is_derive` (one less hypothesis)
+
+- in `exp.v`:
+  + lemma `derivable_powR`
 
 ### Deprecated
 
diff --git a/theories/exp.v b/theories/exp.v
index f0d409c538..ebca7c8c7e 100644
--- a/theories/exp.v
+++ b/theories/exp.v
@@ -1088,11 +1088,9 @@ apply: (@cvg_comp _ _ _ _ _ _ (@ninfty_nbhs R)).
 exact/cvgNy_compNP/cvgr_expR.
 Unshelve. end_near. Qed.
 
-Lemma derivable_powR v x :
-  {in `]0, +oo[, forall a, derivable (powR ^~ x) a v}.
+Lemma derivable_powR v x : {in `]0, +oo[, forall a, derivable (powR ^~ x) a v}.
 Proof.
-case: (eqVneq v 0)=> [-> y _| ].
-by apply/derivable0.
+have [-> y _|] := eqVneq v 0; first exact/derivable0.
 move=> v0 a; rewrite in_itv/= andbT => a0.
 apply: (@near_eq_derivable _ _ _ (fun a' => expR (x * ln a'))) => //.
   by near=> b; rewrite /powR gt_eqF//; near: b; exact: lt_nbhsr.