proposition: Theorem inbetween_float_ZR_sign : forall x m l, let e := cexp beta fexp x in inbetween_float beta m e (Rabs x) l -> round beta fexp Ztrunc x = F2R (Float beta (cond_Zopp (Rlt_bool x 0) m) e).
proof: Proof. apply inbetween_float_round_sign with (choice := fun s m l => m). exact inbetween_int_ZR_sign. Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket