fact: Definition truncate_FIX t := let '(m, e, l) := t in let k := (emin - e)%Z in if Zlt_bool 0 k then let p := Zpower beta k in (Z.div m p, (e + k)%Z, new_location p (Zmod m p) l) else t.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket