fact: Definition Fmul_aux {beta} (x y : float beta) : ufloat beta := match x, y with | Fnan, _ => Unan | _, Fnan => Unan | Fzero, _ => Uzero | _, Fzero => Uzero | Float sx mx ex, Float sy my ey => Ufloat (xorb sx sy) (Pmult mx my) (ex + ey) pos_Eq end.
imports: Coq(Reals Bool ZArith) Flocq(Zaux Raux Div Sqrt) Xreal Basic