From 16f7540060ff4da046f011ac92b09e429140deb2 Mon Sep 17 00:00:00 2001
From: Takafumi Saikawa <tscompor@gmail.com>
Date: Wed, 7 Aug 2024 22:52:49 +0900
Subject: [PATCH] rat_in_itvoo need not be restricted to realTypes (#1286)

* rat_in_itvoo need not be restricted to realTypes
---
 CHANGELOG_UNRELEASED.md | 2 ++
 theories/reals.v        | 2 +-
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 67bb43c3b..698794d56 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -9,6 +9,8 @@
 ### Renamed
 
 ### Generalized
+- in `reals.v`:
+  + lemma `rat_in_itvoo`
 
 ### Deprecated
 
diff --git a/theories/reals.v b/theories/reals.v
index a989068bb..c2dd629c5 100644
--- a/theories/reals.v
+++ b/theories/reals.v
@@ -677,7 +677,7 @@ rewrite /bound_div (ltNge y 0) y0/= -mulr_natl -ltr_pdivrMr//.
 by rewrite archi_boundP// (divr_ge0 _(ltW _)).
 Qed.
 
-Lemma rat_in_itvoo (R : realType) (x y : R) :
+Lemma rat_in_itvoo (R : archiFieldType) (x y : R) :
   x < y -> exists q, ratr q \in `]x, y[.
 Proof.
 move=> xy; move: (xy); rewrite -subr_gt0.