proposition: Lemma error_le_ulp_round : forall { Hm : Monotone_exp fexp } rnd { Zrnd : Valid_rnd rnd } x, (Rabs (round beta fexp rnd x - x) <= ulp (round beta fexp rnd x))%R.
proof: Proof. intros Mexp rnd Vrnd x. destruct (Req_dec x 0) as [Zx|Nzx]. { rewrite Zx, round_0; [|exact Vrnd]. unfold Rminus; rewrite Ropp_0, Rplus_0_l, Rabs_R0; apply ulp_ge_0. } now apply Rlt_le, error_lt_ulp_round. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop