proposition: Lemma err_add_: forall x1 y1 e1 x2 y2 e2, err x1 y1 e1 -> err x2 y2 e2 -> 0 <= y1 -> 0 <= y2 -> format x1 -> format x2 -> err (round_flt (x1+x2)) (y1+y2) (eps + (1+eps)*(Rmax e1 e2)).
proof: Proof. Proof with auto with typeclass_instances. intros x1 y1 e1 x2 y2 e2 H1 H2 Hy1 Hy2 Fx1 Fx2. replace (round_flt (x1+x2) - (y1+y2)) with ((round_flt (x1+x2)-(x1+x2))+(x1+x2 - (y1+y2))) by ring. apply Rle_trans with (1:=Rabs_triang _ _). apply Rle_trans with (eps*Rabs (x1+x2) + Rabs (x1 + x2 - (y1 + y2))). apply Rplus_le_compat_r. now apply err_add_no_err. rewrite Rmult_plus_distr_r. pattern (x1+x2) at 1; replace (x1+x2) with ((x1 + x2 - (y1 + y2))+(y1+y2)) by ring. apply Rle_trans with (eps * Rabs (y1 + y2) + (1 + eps) * (Rabs (x1 + x2 - (y1 + y2)))). apply Rle_trans with (eps * Rabs (x1 + x2 - (y1 + y2)) + eps *Rabs (y1 + y2) + Rabs (x1 + x2 - (y1 + y2))). apply Rplus_le_compat_r. rewrite <- Rmult_plus_distr_l. apply Rmult_le_compat_l. apply epsPos. apply Rabs_triang. right; ring. apply Rplus_le_compat_l. rewrite Rmult_assoc. apply Rmult_le_compat_l. apply Fourier_util.Rle_zero_pos_plus1, epsPos. replace (x1 + x2 - (y1 + y2)) with ((x1-y1)+(x2-y2)) by ring. apply Rle_trans with (1:=Rabs_triang _ _). apply Rle_trans with (e1*Rabs y1 + e2* Rabs y2). now apply Rplus_le_compat. apply Rle_trans with (Rmax e1 e2*Rabs y1 + Rmax e1 e2 * Rabs y2). apply Rplus_le_compat; apply Rmult_le_compat_r; try apply Rabs_pos. apply Rmax_l. apply Rmax_r. rewrite <- Rmult_plus_distr_l. right; apply f_equal. repeat rewrite Rabs_right; try reflexivity; apply Rle_ge; try assumption. now apply Rplus_le_le_0_compat. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)