fact: Definition Fplus (f1 f2 : float beta) := let (m1, e1) := f1 in let (m2, e2) := f2 in if Zeq_bool m1 0 then (m2, e2, loc_Exact) else if Zeq_bool m2 0 then (m1, e1, loc_Exact) else let p1 := (Zdigits beta m1 + e1)%Z in let p2 := (Zdigits beta m2 + e2)%Z in if Zle_bool 2 (Z.abs (p1 - p2)) then let e := Z.min (Z.max e1 e2) (fexp (Z.max p1 p2 - 1)) in let (m, l) := if Zlt_bool e1 e then Fplus_core m2 e2 m1 e1 e else Fplus_core m1 e1 m2 e2 e in (m, e, l) else let (m, e) := Fplus f1 f2 in (m, e, loc_Exact).
imports: Coq(ZArith Reals Lia) Core Bracket Operations Round