rat_in_itvoo need not be restricted to realTypes

math-comp · Aug 7, 2024 · 0c7d8a1 · 0c7d8a1
1 parent 107266f
commit 0c7d8a1
Showing 1 changed file with 1 addition and 1 deletion.
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.