proposition: Theorem relative_error_N_FLX : forall x, (Rabs (round beta (FLX_exp prec) (Znearest choice) x - x) <= /2 * bpow (-prec + 1) * Rabs x)%R.
proof: Proof. Proof with auto with typeclass_instances. intros 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. destruct (mag beta x) as (ex, He). specialize (He Hx). apply relative_error_N with (ex - 1)%Z... intros k _. apply relative_error_FLX_aux. apply He. Qed.
imports: Coq(ZArith Reals Psatz) Core