proposition: Theorem round_trunc_sign_any_correct' : forall x m e l, inbetween_float beta m e (Rabs x) l -> (e <= cexp beta fexp x)%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. rewrite <- cexp_abs in He. generalize (truncate_correct' (Rabs x) m e l (Rabs_pos _) Hl He). destruct (truncate (m, e, l)) as [[m' e'] l']. intros [H1 H2]. apply round_sign_any_correct. exact H1. destruct H2 as [H2|[H2 H3]]. left. now rewrite <- cexp_abs. right. apply (conj H2). now apply generic_format_abs_inv. Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket