fact: Definition plus (x y : float beta) := let (m, e) := Fplus x y in let s := Zlt_bool m 0 in let '(m', e', l) := truncate beta fexp (Z.abs m, e, loc_Exact) in Float beta (cond_Zopp s (choice s m' l)) e'.
imports: Coq(ZArith Reals) Flocq(Core Bracket Round Operations Div Sqrt)