proposition: Theorem truncate_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 -> let '(m', e', l') := truncate (m, e, l) in inbetween_float beta m' e' x l' /\ (e' = cexp beta fexp x \/ (l' = loc_Exact /\ format x)).
proof: Proof. intros x m e l Hx H1 H2. apply truncate_correct' with (1 := Hx) (2 := H1). now apply cexp_inbetween_float_loc_Exact with (2 := H1). Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket