proposition: Theorem relative_error_N_F2R_emin : forall m, let x := F2R (Float beta m emin) in (Rabs (round beta fexp (Znearest choice) x - x) <= /2 * bpow (-p + 1) * Rabs x)%R.
proof: Proof. Proof with auto with typeclass_instances. intros m x. destruct (Req_dec x 0) as [Hx|Hx]. rewrite Hx, round_0... unfold Rminus. rewrite Rplus_0_l, Rabs_Ropp, Rabs_R0. rewrite Rmult_0_r. apply Rle_refl. apply relative_error_N. unfold x. rewrite <- F2R_Zabs. apply bpow_le_F2R. apply lt_F2R with beta emin. rewrite F2R_0, F2R_Zabs. now apply Rabs_pos_lt. Qed.
imports: Coq(ZArith Reals Psatz) Core