proposition: Theorem ulp_DN : forall x, (0 <= x)%R -> ulp (round beta fexp Zfloor x) = ulp x.
proof: Proof. Proof with auto with typeclass_instances. intros x [Hx|Hx]. - rewrite (ulp_neq_0 x) by now apply Rgt_not_eq. destruct (round_ge_generic beta fexp Zfloor 0 x) as [Hd|Hd]. apply generic_format_0. now apply Rlt_le. + rewrite ulp_neq_0 by now apply Rgt_not_eq. now rewrite cexp_DN with (2 := Hd). + rewrite <- Hd. unfold cexp. destruct (mag beta x) as [e He]. simpl. specialize (He (Rgt_not_eq _ _ Hx)). apply sym_eq in Hd. assert (H := exp_small_round_0 _ _ _ _ _ He Hd). unfold ulp. rewrite Req_bool_true by easy. destruct negligible_exp_spec as [H0|k Hk]. now elim Zlt_not_le with (1 := H0 e). now apply f_equal, fexp_negligible_exp_eq. - rewrite <- Hx, round_0... Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop