proposition: Lemma plus_error_aux : forall x y, (cexp beta fexp x <= cexp beta fexp y)%Z -> format x -> format y -> format (round beta fexp (Znearest choice) (x + y) - (x + y))%R.
proof: Proof. intros x y. set (ex := cexp beta fexp x). set (ey := cexp beta fexp y). intros He Hx Hy. destruct (Req_dec (round beta fexp (Znearest choice) (x + y) - (x + y)) R0) as [H0|H0]. rewrite H0. apply generic_format_0. set (mx := Ztrunc (scaled_mantissa beta fexp x)). set (my := Ztrunc (scaled_mantissa beta fexp y)). assert (Hxy: (x + y)%R = F2R (Float beta (mx + my * beta ^ (ey - ex)) ex)). rewrite Hx, Hy. fold mx my ex ey. rewrite <- F2R_plus. unfold Fplus. simpl. now rewrite Zle_imp_le_bool with (1 := He). rewrite Hxy. destruct (round_repr_same_exp (Znearest choice) (mx + my * beta ^ (ey - ex)) ex) as (mxy, Hxy'). rewrite Hxy'. assert (H: (F2R (Float beta mxy ex) - F2R (Float beta (mx + my * beta ^ (ey - ex)) ex))%R = F2R (Float beta (mxy - (mx + my * beta ^ (ey - ex))) ex)). now rewrite <- F2R_minus, Fminus_same_exp. rewrite H. apply generic_format_F2R. intros _. apply monotone_exp. rewrite <- H, <- Hxy', <- Hxy. apply mag_le_abs. exact H0. pattern x at 3 ; replace x with (-(y - (x + y)))%R by ring. rewrite Rabs_Ropp. now apply (round_N_pt beta _ choice (x + y)). Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative