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