fact: Definition Fdiv (x y : float beta) := let (m1, e1) := x in let (m2, e2) := y in let e' := ((Zdigits beta m1 + e1) - (Zdigits beta m2 + e2))%Z in let e := Z.min (Z.min (fexp e') (fexp (e' + 1))) (e1 - e2) in let '(m, l) := Fdiv_core m1 e1 m2 e2 e in (m, e, l).
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Generic_fmt Float_prop Digits Bracket