proposition: Theorem relative_error_N_ex : forall x, (bpow emin <= Rabs x)%R -> exists eps, (Rabs eps <= /2 * bpow (-p + 1))%R /\ round beta fexp (Znearest choice) x = (x * (1 + eps))%R.
proof: Proof. Proof with auto with typeclass_instances. intros x Hx. apply relative_error_le_conversion... apply Rlt_le. apply Rmult_lt_0_compat. apply Rinv_0_lt_compat. now apply IZR_lt. apply bpow_gt_0. now apply relative_error_N. Qed.
imports: Coq(ZArith Reals Psatz) Core