rat_in_itvoo need not be restricted to realTypes (#1286)

* rat_in_itvoo need not be restricted to realTypes
math-comp · Aug 7, 2024 · 16f7540 · 16f7540
1 parent 107266f
commit 16f7540
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 1 deletion.
diff --git 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
@@ -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.