proposition: Lemma ulp_neq_0 : forall x, x <> 0%R -> ulp x = bpow (cexp beta fexp x).
proof: Proof. intros x Hx. unfold ulp; case (Req_bool_spec x); trivial. intros H; now contradict H. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop