diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 0d911f46c..8d8613d1a 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.v`:
+  + multirule `RealsE` to convert from Stdlib reals to Analysis ones
+
 - in `Rstruct_topology.v`:
   + lemma `RlnE`
 
diff --git a/reals_stdlib/Rstruct.v b/reals_stdlib/Rstruct.v
index ec34553cf..20f5321a5 100644
--- a/reals_stdlib/Rstruct.v
+++ b/reals_stdlib/Rstruct.v
@@ -539,6 +539,10 @@ Qed.
 Lemma factE n : fact n = n`!.
 Proof. by elim: n => //= n ih; rewrite factS mulSn ih. Qed.
 
+Definition RealsE := (RplusE, RminusE, RmultE, RoppE, RinvE, RdivE, INRE,
+  Pos_to_natE, IZRposE, RsqrtE, RpowE, RmaxE, RminE, RabsE, RdistE,
+  sum_f_R0E, factE).
+
 Section bigmaxr.
 Context {R : realDomainType}.