From 14e2fbbb4c2542feeabf2ed44cc8ba4941526c7e Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Wed, 4 Feb 2026 13:55:22 +0100
Subject: [PATCH] Add a RealsE multirule

---
 CHANGELOG_UNRELEASED.md | 3 +++
 reals_stdlib/Rstruct.v  | 4 ++++
 2 files changed, 7 insertions(+)

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}.