fact: Definition round_mode m := match m with | mode_NE => ZnearestE | mode_ZR => Ztrunc | mode_DN => Zfloor | mode_UP => Zceil | mode_NA => ZnearestA end.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative