From 1e80f29f0bb26b44a696b8d23fc3e4bbe6c34081 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 01/11] Added lemma to swap mathcomp natural log with Rocqs
 natural log

---
 CHANGELOG_UNRELEASED.md            |  3 +++
 analysis_stdlib/Rstruct_topology.v | 22 ++++++++++++++++++++++
 2 files changed, 25 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index e5df5f1a1a..81faff5455 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -4,6 +4,9 @@
 
 ### Added
 
+- in `analysis_stdlib/Rstruct_topology.v`:
+  + lemma `RlnE`
+
 - in `classical_sets.v`:
   + lemma `nonemptyPn`
 
diff --git a/analysis_stdlib/Rstruct_topology.v b/analysis_stdlib/Rstruct_topology.v
index e2693b4ad2..6fe8105165 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.
@@ -107,3 +109,23 @@ Unshelve. all: by end_near. Qed.
 End RexpE.
 
 Definition RexpE := RexpE.RexpE.
+
+Lemma RlnE (x : R) : 0 < x -> Rpower.ln x = exp.ln x.
+Proof.
+rewrite /ln /Rpower.ln /= /Rln /=.
+case: (Rlt_dec 0 x) => [/= x_pos | ? /RltP //].
+have ln_res := ln_exists x x_pos.
+have : ln_exists x x_pos = ln_res.
+  apply: eq_sig.
+    case: ln_res => y x_ey.
+    case: (ln_exists x x_pos) => z z_ey /=.
+    apply:exp.expR_inj.
+    rewrite -!RexpE.
+    by rewrite -z_ey -x_ey.
+  case: ln_res.
+  by case: (ln_exists x x_pos) => [y ?] z ? /= ?; subst y.
+move=> -> _ /=.
+move: ln_res => [y x_ey].
+rewrite x_ey RexpE.
+by rewrite exp.expRK.
+Qed.

From 1934bf3c97919ef63b21467c4e71e9ee600dca40 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 02/11] 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 440a1497e2..83280b7cca 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 2638f48e81eb7f16455214b68c3ba5065189faa9 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 03/11] linting

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

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 9d8675134e..576f11a227 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -10,7 +10,14 @@
 - in set_interval.v
   + `itv_is_open_unbounded`, `itv_is_oo`, `itv_open_ends` (Prop to bool)
 
+- 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 38cf34e941..8f63e34c87 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 83280b7cca..d1aaf022e7 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 83a8b2be5a624d0eb1241f2f39d4eedbefc6318c Mon Sep 17 00:00:00 2001
From: Alistair Sirman <alistair.sirman@gmail.com>
Date: Wed, 28 Jan 2026 09:55:09 +0000
Subject: [PATCH 04/11] Generalised Lemma and shortened

---
 analysis_stdlib/Rstruct_topology.v | 23 ++++++-----------------
 1 file changed, 6 insertions(+), 17 deletions(-)

diff --git a/analysis_stdlib/Rstruct_topology.v b/analysis_stdlib/Rstruct_topology.v
index 6fe8105165..47ddf19f89 100644
--- a/analysis_stdlib/Rstruct_topology.v
+++ b/analysis_stdlib/Rstruct_topology.v
@@ -110,22 +110,11 @@ End RexpE.
 
 Definition RexpE := RexpE.RexpE.
 
-Lemma RlnE (x : R) : 0 < x -> Rpower.ln x = exp.ln x.
+Lemma RlnE (x : R) : Rpower.ln x = exp.ln x.
 Proof.
-rewrite /ln /Rpower.ln /= /Rln /=.
-case: (Rlt_dec 0 x) => [/= x_pos | ? /RltP //].
-have ln_res := ln_exists x x_pos.
-have : ln_exists x x_pos = ln_res.
-  apply: eq_sig.
-    case: ln_res => y x_ey.
-    case: (ln_exists x x_pos) => z z_ey /=.
-    apply:exp.expR_inj.
-    rewrite -!RexpE.
-    by rewrite -z_ey -x_ey.
-  case: ln_res.
-  by case: (ln_exists x x_pos) => [y ?] z ? /= ?; subst y.
-move=> -> _ /=.
-move: ln_res => [y x_ey].
-rewrite x_ey RexpE.
-by rewrite exp.expRK.
+rewrite /Rpower.ln /Rln.
+have [xle0|xgt0] := leP x 0.
+  by case: Rlt_dec => //= /[dup] /RltP + ?; rewrite exp.ln0// ltNge xle0.
+case: (Rlt_dec 0 x) => [/= ? | /RltP/[!xgt0]//].
+by case: ln_exists => y ->; rewrite RexpE exp.expRK.
 Qed.

From 6d24c456db2f6239680d170abe9a8d1718616ee1 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 05/11] 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 8f63e34c87..8347f42424 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 d1aaf022e7..9da7acf73e 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 8ef362ebc9d4796469fccd5ec3ec323d4103cd0c 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 06/11] Revert "Merge branch 'ln_eq_Rln' into HEAD"

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

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index a79a9a0478..576f11a227 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -3,120 +3,6 @@
 ## [Unreleased]
 
 ### Added
-
-- in `analysis_stdlib/Rstruct_topology.v`:
-  + lemma `RlnE`
-
-- in `classical_sets.v`:
-  + lemma `nonemptyPn`
-
-- in `cardinality.v`:
-  + lemma `infinite_setD`
-
-- in `convex.v`:
-  + lemmas `convN`, `conv_le`
-
-- in `normed_module.v`:
-  + lemma `limit_point_infinite_setP`
-- in `measure_negligible.v`:
-  + definition `null_set` with notation `_.-null_set`
-  + lemma `subset_null_set`
-  + lemma `negligible_null_set`
-  + lemma `measure0_null_setP`
-  + lemma `null_setU`
-  + definition `null_dominates`
-  + lemma `null_dominates_trans`
-  + lemma `null_content_dominatesP`
-
-- in `charge.v`:
-  + definition `charge_dominates`
-  + lemma `charge_null_dominatesP`
-  + lemma `content_charge_dominatesP`
-
-- in `sequences.v`:
-  + lemma `increasing_seq_injective`
-  + definition `adjacent_set`
-  + lemmas `adjacent_sup_inf`, `adjacent_sup_inf_unique`
-  + definition `cut`
-  + lemmas `cut_adjacent`, `infinite_bounded_limit_point_nonempty`
-
-- in `measurable_structure.v`:
-  + lemma `dynkin_induction``
-
-- in `lebesgue_integral_fubini.v`:
-  + definition `product_subprobability`
-  + lemma `product_subprobability_setC`
-
-- in `lebesgue_integral_theory/lebesgue_integrable.v`
-  + lemma `null_set_integrable`
-
-- new file `lebesgue_integral_theory/giry.v`
-  + definition `measure_eq`
-  + definition `giry`
-  + definition `giry_ev`
-  + definition `giry_measurable`
-  + definition `preimg_giry_ev`
-  + definition `giry_display`
-  + lemma `measurable_giry_ev`
-  + definition `giry_int`
-  + lemmas `measurable_giry_int`, `measurable_giry_codensity`
-  + definition `giry_map`
-  + lemmas `measurable_giry_map`, `giry_int_map`, `giry_map_dirac`
-  + definition `giry_ret`
-  + lemmas `measurable_giry_ret`, `giry_int_ret`
-  + definition `giry_join`
-  + lemmas `measurable_giry_join`, `sintegral_giry_join`, `giry_int_join`
-  + definition `giry_bind`
-  + lemmas `measurable_giry_bind`, `giry_int_bind`
-  + lemmas `giry_joinA`, `giry_join_id1`, `giry_join_id2`, `giry_map_zero`
-  + definition `giry_prod`
-  + lemmas `measurable_giry_prod`, `giry_int_prod1`, `giry_int_prod2`
-
-- in `measurable_realfun.v`:
-  + lemma `measurable_funN`
-  + lemmas `nondecreasing_measurable`, `nonincreasing_measurable`
-- in `subspace_topology.v`:
-  + definition `from_subspace`
-- in `topology_structure.v`:
-  + definition `isolated`
-  + lemma `isolatedS`
-  + lemma `disjoint_isolated_limit_point`
-  + lemma `closure_isolated_limit_point`
-
-- in `separation_axioms.v`:
-  + lemma `perfectP`
-
-- in `cardinality.v`:
-  + lemmas `finite_setX_or`, `infinite_setX`
-  + lemmas `infinite_prod_rat`, ``card_rat2`
-
-- in `normed_module.v`:
-  + lemma `open_subball_rat`
-  + fact `isolated_rat_ball`
-  + lemma `countable_isolated`
-- in `normed_module.v`:
-  + lemma `limit_point_setD`
-
-- in `reals.v`:
-  + lemma `nat_has_minimum`
-
-- in `sequences.v`:
-  + lemma `cluster_eventuallyP`
-  + lemmas `cluster_eventually_cvg`, `limit_point_cluster_eventually`
-
-- in `lebesgue_integrable.v`:
-  + lemma `integrable_set0`
-
-- in `lebesgue_integrable.v`:
-  + lemma `integrable_norm`
-- in `order_topology.v`:
-  + structures `POrderedNbhs`, `POrderedTopological`, `POrderedUniform`, `POrderedPseudoMetric`,
-    `POrderedPointedTopological`
-- in `num_topology.v`:
-  + lemmas `continuous_rsubmx`, `continuous_lsubmx`
-
-- in `derive.v`:
-  + lemmas `differentiable_rsubmx`, `differentiable_lsubmx`
 - in set_interval.v
   + definitions `itv_is_closed_unbounded`, `itv_is_cc`, `itv_closed_ends`
 
diff --git a/analysis_stdlib/Rstruct_topology.v b/analysis_stdlib/Rstruct_topology.v
index 47ddf19f89..e2693b4ad2 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.
@@ -109,12 +107,3 @@ Unshelve. all: by end_near. Qed.
 End RexpE.
 
 Definition RexpE := RexpE.RexpE.
-
-Lemma RlnE (x : R) : Rpower.ln x = exp.ln x.
-Proof.
-rewrite /Rpower.ln /Rln.
-have [xle0|xgt0] := leP x 0.
-  by case: Rlt_dec => //= /[dup] /RltP + ?; rewrite exp.ln0// ltNge xle0.
-case: (Rlt_dec 0 x) => [/= ? | /RltP/[!xgt0]//].
-by case: ln_exists => y ->; rewrite RexpE exp.expRK.
-Qed.

From 9ecf8022feb5e260da7453db90e9ea2148e91efc 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 07/11] Updated changelog

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

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 576f11a227..ac9cd99495 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -11,10 +11,10 @@
   + `itv_is_open_unbounded`, `itv_is_oo`, `itv_open_ends` (Prop to bool)
 
 - 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 1524a05324d6f91da98e2008add1a06608bb9dff 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 08/11] 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 ac9cd99495..6b4a0d77fb 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -17,7 +17,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 8347f42424..e4344771d5 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 9da7acf73e..e178662a9c 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 540b1df54dd33a600f737143ccba4a8b267b1eef 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 09/11] 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 e4344771d5..69ff221dfd 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 611fb2ea23d465e4e39faeeaadcebe25566cd480 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 10/11] Fixed error

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

diff --git a/theories/derive.v b/theories/derive.v
index e178662a9c..605a45cb8a 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 614b6289861f2dc864fca3eeb13c96f7c93453d4 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 11/11] 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 e3a5271069..6f181f6504 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.