proposition: Lemma FLT_plus_error_N_ex : forall x y, generic_format beta (FLT_exp emin prec) x -> generic_format beta (FLT_exp emin prec) y -> exists eps, (Rabs eps <= u_ro beta prec / (1 + u_ro beta prec))%R /\ round beta (FLT_exp emin prec) (Znearest choice) (x + y) = ((x + y) * (1 + eps))%R.
proof: Proof. intros x y Fx Fy. assert (Pb := u_rod1pu_ro_pos beta prec). destruct (Rle_or_lt (bpow (emin + prec - 1)) (Rabs (x + y))) as [M|M]. { destruct (relative_error_N_FLX'_ex beta prec prec_gt_0_ choice (x + y)) as (d, (Bd, Hd)). now exists d; split; [exact Bd|]; rewrite <- Hd; apply round_FLT_FLX. } exists 0%R; rewrite Rabs_R0; split; [exact Pb|]; rewrite Rplus_0_r, Rmult_1_r. apply round_generic; [apply valid_rnd_N|]. apply FLT_format_plus_small; [exact Fx|exact Fy|]. apply Rlt_le, (Rlt_le_trans _ _ _ M), bpow_le; lia. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative