proposition: Fact ext4 x : Rabs (round r phi (Znearest choice) x - x) <= / 2 * ulp r phi x.
proof: Proof. assert (H : generic_format r phi x \/ ~ generic_format r phi x). unfold generic_format, F2R; simpl. set (y := _ * _); case (Req_dec x y); auto. destruct H. set (y := _ - _); replace y with 0. rewrite Rabs_R0. apply Rmult_le_pos; try lra; apply ulp_ge_0. unfold y; rewrite round_generic; auto; try ring. apply valid_rnd_N. destruct (round_N_pt r phi choice x) as (Hr1, Hr2). assert (H1 := generic_format_round r phi Zfloor x). assert (H2 := generic_format_round r phi Zceil x). assert (H3 := Hr2 _ H1). assert (H4 := Hr2 _ H2). assert (H5 := round_UP_DN_ulp _ _ _ H). assert (H6 := round_DN_UP_lt _ _ _ H). destruct (round_DN_or_UP r phi (Znearest choice) x). revert H3 H4. split_Rabs; try lra. split_Rabs; try lra. Qed.
imports: Psatz ZArith Reals SpecFloat Flocq(FTZ Core Operations BinarySingleNaN Binary Bits)