proposition: Theorem relative_error_N_FLT_round_F2R_emin : forall m, let x := F2R (Float beta m emin) in (Rabs (round beta (FLT_exp emin prec) (Znearest choice) x - x) <= /2 * bpow (-prec + 1) * Rabs (round beta (FLT_exp emin prec) (Znearest choice) x))%R.
proof: Proof. Proof with auto with typeclass_instances. intros m x. destruct (Rlt_or_le (Rabs x) (bpow (emin + prec - 1))) as [Hx|Hx]. rewrite round_generic... unfold Rminus. rewrite Rplus_opp_r, Rabs_R0. apply Rmult_le_pos. apply Rmult_le_pos. apply Rlt_le. apply (RinvN_pos 1). apply bpow_ge_0. apply Rabs_pos. apply generic_format_FLT_FIX... apply Rlt_le. apply Rlt_le_trans with (1 := Hx). apply bpow_le. apply Zle_pred. apply generic_format_FIX. now exists (Float beta m emin). apply relative_error_N_round with (emin := (emin + prec - 1)%Z)... apply relative_error_FLT_aux. Qed.
imports: Coq(ZArith Reals Psatz) Core