proposition: Theorem inbetween_float_ZR : forall x m l, let e := cexp beta fexp x in inbetween_float beta m e x l -> round beta fexp Ztrunc x = F2R (Float beta (cond_incr (round_ZR (Zlt_bool m 0) l) m) e).
proof: Proof. apply inbetween_float_round with (choice := fun m l => cond_incr (round_ZR (Zlt_bool m 0) l) m). exact inbetween_int_ZR. Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket