From 0c7d8a1e733231dcb8a3f212651e3b7d4e4863b8 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Wed, 7 Aug 2024 17:25:33 +0900 Subject: [PATCH 1/2] rat_in_itvoo need not be restricted to realTypes --- theories/reals.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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. From 1c6892bb668dff54590e19b83fda7ee3ddefd93c Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Wed, 7 Aug 2024 20:57:56 +0900 Subject: [PATCH 2/2] changelog --- CHANGELOG_UNRELEASED.md | 2 ++ 1 file changed, 2 insertions(+) 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