proposition: Lemma FLT_plus_error_N_round_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)%R /\ (x + y = round beta (FLT_exp emin prec) (Znearest choice) (x + y) * (1 + eps))%R.
proof: Proof. intros x y Fx Fy. now apply relative_error_N_round_ex_derive, FLT_plus_error_N_ex. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative