fact: Definition overflow_to_inf m s := match m with | mode_NE => true | mode_NA => true | mode_ZR => false | mode_UP => negb s | mode_DN => s end.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative