proposition: Lemma err_mult: forall x1 y1 e1 x2 y2 e2, err x1 y1 e1 -> err x2 y2 e2 -> err (round_flx (x1*x2)) (y1*y2) (eps+(1+eps)*(e1+e2+e1*e2)).
proof: Proof. Proof with auto with typeclass_instances. intros x1 y1 e1 x2 y2 e2 H1 H2. replace (round_flx (x1 * x2) - y1*y2) with ((round_flx (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. apply err_init. rewrite Rmult_plus_distr_r. apply Rle_trans with (eps*Rabs (y1 * y2) + (1+eps)*Rabs (x1 * x2 - y1 * y2)). pattern (x1*x2) at 1; replace (x1*x2) with ((x1 * x2 - (y1 * y2))+(y1*y2)) by ring. 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. rewrite 2!Rmult_plus_distr_r. replace (x1*x2-y1*y2) with ((x1-y1)*y2+(x2-y2)*y1+(x1-y1)*(x2-y2)) by ring. apply Rle_trans with (1:=Rabs_triang _ _). apply Rplus_le_compat. apply Rle_trans with (1:=Rabs_triang _ _). apply Rplus_le_compat. rewrite 2!Rabs_mult. rewrite <- Rmult_assoc. apply Rmult_le_compat_r. apply Rabs_pos. exact H1. rewrite 2!Rabs_mult. rewrite (Rmult_comm _ (Rabs y2)). rewrite <- Rmult_assoc. apply Rmult_le_compat_r. apply Rabs_pos. exact H2. apply Rle_trans with ((e1*Rabs y1)*(e2*Rabs y2)). rewrite Rabs_mult. apply Rmult_le_compat; try assumption; apply Rabs_pos. rewrite Rabs_mult; right; ring. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)