proposition: Theorem error_le_ulp : forall rnd { Zrnd : Valid_rnd rnd } x, (Rabs (round beta fexp rnd x - x) <= ulp x)%R.
proof: Proof. Proof with auto with typeclass_instances. intros rnd Zrnd x. case (Req_dec x 0). intros Zx; rewrite Zx, round_0... unfold Rminus; rewrite Rplus_0_l, Ropp_0, Rabs_R0. apply ulp_ge_0. intros Zx; left. now apply error_lt_ulp. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop