fact: Definition ulp x := match Req_bool x 0 with | true => match negligible_exp with | Some n => bpow (fexp n) | None => 0%R end | false => bpow (cexp beta fexp x) end.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop