fact: Definition Btrunc (x : binary_float) := match x with | B754_finite s m e _ => cond_Zopp s (SFnearbyint_binary_aux mode_ZR s m e) | _ => 0%Z end.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative