proposition: Theorem round_trunc_any_correct : forall x m e l, (0 <= x)%R -> inbetween_float beta m e 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 (choice m' l') e').
proof: Proof. intros x m e l Hx Hl He. generalize (truncate_correct x m e l Hx Hl He). destruct (truncate (m, e, l)) as ((m', e'), l'). intros (H1, H2). now apply round_any_correct. Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket