proposition: Lemma err_add2_: forall x x2 y2 e2, err x2 y2 e2 -> format x -> format x2 -> 0 <= e2 -> 0 <= y2 <= x -> err (round_flt (x+x2)) (x+y2) (eps*(1+e2)+e2/2).
proof: Proof. Proof with auto with typeclass_instances. intros x x2 y2 e2 H2 Z1 Z2 H (Y1,Y2). replace (round_flt (x+x2) - (x+y2)) with ((round_flt (x+x2)-(x+x2))+(x2 - y2)) by ring. apply Rle_trans with (1:=Rabs_triang _ _). rewrite Rmult_plus_distr_r. apply Rplus_le_compat. apply Rle_trans with (eps*Rabs (x+x2)). now apply err_add_no_err. rewrite Rmult_assoc with (r3:=Rabs (x + y2)). apply Rmult_le_compat_l. apply epsPos. replace (x+x2) with ((x + y2) +(x2-y2)) by ring. apply Rle_trans with (1:=Rabs_triang _ _). rewrite Rmult_plus_distr_r. rewrite Rmult_1_l. apply Rplus_le_compat_l. apply Rle_trans with (1:=H2). apply Rmult_le_compat_l. apply H. rewrite 2!Rabs_right. rewrite <- (Rplus_0_l y2). apply Rplus_le_compat; auto with real. apply Rle_trans with y2; assumption. apply Rle_ge, Rplus_le_le_0_compat. apply Rle_trans with y2; assumption. assumption. apply Rle_ge; assumption. apply Rle_trans with (1:=H2). unfold Rdiv; rewrite Rmult_assoc. apply Rmult_le_compat_l. apply H. apply Rmult_le_reg_l with 2; auto with real. rewrite <- Rmult_assoc, Rinv_r. 2: now apply IZR_neq. rewrite 2!Rabs_pos_eq ; lra. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)