fact: Definition Frem_aux {beta} (x y : float beta) := match x, y with | Fnan, _ => (Fnan, Unan) | _, Fnan => (Fnan, Unan) | _, Fzero => (Fnan, Unan) | Fzero, _ => (Fzero, Uzero) | Float sx mx ex, Float sy my ey => let s := xorb sx sy in match (ex - ey)%Z with | Zpos nb => Frem_aux1 beta (shift beta mx nb) my s ey | Z0 => Frem_aux1 beta mx my s ex | Zneg nb => Frem_aux1 beta mx (shift beta my nb) s ex end end.
imports: Coq(Reals Bool ZArith) Flocq(Zaux Raux Div Sqrt) Xreal Basic