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..47ddf19f89 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,12 @@ 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.