proposition: Theorem relative_error_N : forall x, (bpow emin <= Rabs x)%R -> (Rabs (round beta fexp (Znearest choice) x - x) <= /2 * bpow (-p + 1) * Rabs x)%R.
proof: Proof. intros x Hx. apply Rle_trans with (/2 * ulp beta fexp x)%R. now apply error_le_half_ulp. rewrite Rmult_assoc. apply Rmult_le_compat_l. apply Rlt_le. apply Rinv_0_lt_compat. now apply IZR_lt. assert (Hx': (x <> 0)%R). intros H. apply Rlt_not_le with (2 := Hx). rewrite H, Rabs_R0. apply bpow_gt_0. rewrite ulp_neq_0; trivial. unfold cexp. destruct (mag beta x) as (ex, He). simpl. specialize (He Hx'). apply Rle_trans with (bpow (-p + 1) * bpow (ex - 1))%R. rewrite <- bpow_plus. apply bpow_le. assert (emin < ex)%Z. apply (lt_bpow beta). apply Rle_lt_trans with (2 := proj2 He). exact Hx. generalize (Hmin ex). lia. apply Rmult_le_compat_l. apply bpow_ge_0. apply He. Qed.
imports: Coq(ZArith Reals Psatz) Core