fact: Definition float_to_ufloat {beta} (x : float beta) : ufloat beta := match x with | Fnan => Unan | Fzero => Uzero | Float s m e => Ufloat s m e pos_Eq end.
imports: Coq(Reals Bool ZArith) Flocq(Zaux Raux Div Sqrt) Xreal Basic