Commit 58e8dca9 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Added function inbetween_float_bounds.

parent 4ef67160
......@@ -465,6 +465,22 @@ Notation format := (generic_format beta fexp).
Definition inbetween_float m e x l :=
inbetween (F2R (Float beta m e)) (F2R (Float beta (m + 1) e)) x l.
Theorem inbetween_float_bounds :
forall x m e l,
inbetween_float m e x l ->
(F2R (Float beta m e) <= x < F2R (Float beta (m + 1) e))%R.
Proof.
intros x m e l [Hx|l' Hx Hl].
rewrite Hx.
split.
apply Rle_refl.
apply F2R_lt_compat.
apply Zlt_succ.
split.
now apply Rlt_le.
apply Hx.
Qed.
Definition inbetween_int m x l :=
inbetween (Z2R m) (Z2R (m + 1)) x l.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment