proposition: 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: Proof. intros x m e l [Hx|l' Hx Hl]. rewrite Hx. split. apply Rle_refl. apply F2R_lt. apply Zlt_succ. split. now apply Rlt_le. apply Hx. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Float_prop