proposition: Theorem ulp_ge_0: forall x, (0 <= ulp x)%R.
proof: Proof. intros x; unfold ulp; case Req_bool_spec; intros. case negligible_exp; intros. apply bpow_ge_0. apply Rle_refl. apply bpow_ge_0. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop