proposition: Fact ext3 x : x <> 0 -> Rabs (round r phi rnd x - x) < ulp r phi x.
proof: Proof. intro NZx. 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, ulp_neq_0; auto; apply bpow_gt_0. unfold y; rewrite round_generic; auto; ring. assert (H1 := round_DN_UP_lt _ _ _ H). assert (H2 := round_UP_DN_ulp _ _ _ H). destruct (round_DN_or_UP r phi rnd x). split_Rabs; lra. split_Rabs; lra. Qed.
imports: Psatz ZArith Reals SpecFloat Flocq(FTZ Core Operations BinarySingleNaN Binary Bits)