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