proposition: Theorem ulp_round : forall { Not_FTZ_ : Exp_not_FTZ fexp}, forall rnd { Zrnd : Valid_rnd rnd } x, ulp (round beta fexp rnd x) = ulp x \/ Rabs (round beta fexp rnd x) = bpow (mag beta x).
proof: Proof. Proof with auto with typeclass_instances. intros Not_FTZ_ rnd Zrnd x. case (Rtotal_order x 0); intros Zx. case (ulp_round_pos (Zrnd_opp rnd) (-x)). now apply Ropp_0_gt_lt_contravar. rewrite ulp_opp, <- ulp_opp. rewrite <- round_opp, Ropp_involutive. intros Y;now left. rewrite mag_opp. intros Y; right. rewrite <- (Ropp_involutive x) at 1. rewrite round_opp, Y. rewrite Rabs_Ropp, Rabs_right... apply Rle_ge, bpow_ge_0. destruct Zx as [Zx|Zx]. left; rewrite Zx; rewrite round_0... rewrite Rabs_right. apply ulp_round_pos... apply Rle_ge, round_ge_generic... apply generic_format_0... now apply Rlt_le. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop