From b96fbf3c5e443dfe9819d1bd2009868a0aa04bfe 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 1/2] 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 9d8675134e..4b30c26a02 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -6,6 +6,9 @@
 - in set_interval.v
   + definitions `itv_is_closed_unbounded`, `itv_is_cc`, `itv_closed_ends`
 
+- in `Rstruct_topology.v`:
+  + lemma `RlnE`
+
 ### Changed
 - in set_interval.v
   + `itv_is_open_unbounded`, `itv_is_oo`, `itv_open_ends` (Prop to bool)
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 ff701072803066d48b5f3930204e93cb25881db6 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 2/2] 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.