fact: Definition FtoR (s : bool) m e := let sm := if s then Zneg m else Zpos m in match e with | Zpos p => IZR (sm * Zpower_pos beta p) | Z0 => IZR sm | Zneg p => (IZR sm / IZR (Zpower_pos beta p))%R end.
imports: Coq(Reals ZArith Psatz) Flocq(Core) Xreal