proposition: Theorem round_trunc_sign_any_correct : forall x m e l, inbetween_float beta m e (Rabs x) l -> (e <= fexp (Zdigits beta m + e))%Z \/ l = loc_Exact -> round beta fexp rnd x = let '(m', e', l') := truncate (m, e, l) in F2R (Float beta (cond_Zopp (Rlt_bool x 0) (choice (Rlt_bool x 0) m' l')) e').
proof: Proof. intros x m e l Hl He. apply round_trunc_sign_any_correct' with (1 := Hl). rewrite <- cexp_abs. apply cexp_inbetween_float_loc_Exact with (2 := Hl) (3 := He). apply Rabs_pos. Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket