fact: Definition sqrt (x : float beta) := if Zlt_bool 0 (Fnum x) then let '(m', e', l) := truncate beta fexp (Fsqrt fexp x) in Float beta (choice false m' l) e' else Float beta 0 0.
imports: Coq(ZArith Reals) Flocq(Core Bracket Round Operations Div Sqrt)