fact: Definition SF2R beta x := match x with | S754_finite s m e => F2R (Float beta (cond_Zopp s (Zpos m)) e) | _ => 0%R end.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative