fact: Definition Fsqrt_aux {beta} prec (f : float beta) : ufloat beta := match f with | Float false m e => match Fsqrt_aux2 beta (Zpos prec) (Zpos m) e with | (Zpos m, e, l) => Ufloat false m e (convert_location l) | _ => Unan end | Float true _ _ => Unan | Fzero => Uzero | Fnan => Unan end.
imports: Coq(Reals Bool ZArith) Flocq(Zaux Raux Div Sqrt) Xreal Basic