fact: Definition UtoX {beta} (f : ufloat beta) := match f with | Uzero => Xreal R0 | Ufloat s m e pos_Eq => Xreal (FtoR beta s m e) | _ => Xnan end.
imports: Coq(Reals Bool ZArith) Flocq(Zaux Raux Div Sqrt) Xreal Basic