proposition: Lemma round_round_plus_aux0_aux_aux : forall (fexp1 fexp2 : Z -> Z), forall x y, (fexp1 (mag x) <= fexp1 (mag y))%Z -> (fexp2 (mag (x + y))%Z <= fexp1 (mag x))%Z -> (fexp2 (mag (x + y))%Z <= fexp1 (mag y))%Z -> generic_format beta fexp1 x -> generic_format beta fexp1 y -> generic_format beta fexp2 (x + y).
proof: Proof. intros fexp1 fexp2 x y Oxy Hlnx Hlny Fx Fy. destruct (Req_dec x 0) as [Zx|Nzx]. - rewrite Zx, Rplus_0_l in Hlny |- *. now apply (generic_inclusion_mag beta fexp1). - destruct (Req_dec y 0) as [Zy|Nzy]. + rewrite Zy, Rplus_0_r in Hlnx |- *. now apply (generic_inclusion_mag beta fexp1). + revert Fx Fy. unfold generic_format at -3, cexp, F2R; simpl. set (mx := Ztrunc (scaled_mantissa beta fexp1 x)). set (my := Ztrunc (scaled_mantissa beta fexp1 y)). intros Fx Fy. set (fxy := Float beta (mx + my * (beta ^ (fexp1 (mag y) - fexp1 (mag x)))) (fexp1 (mag x))). assert (Hxy : x + y = F2R fxy). { unfold fxy, F2R; simpl. rewrite plus_IZR. rewrite Rmult_plus_distr_r. rewrite <- Fx. rewrite mult_IZR. rewrite IZR_Zpower by lia. bpow_simplify. now rewrite <- Fy. } apply generic_format_F2R' with (f := fxy); [now rewrite Hxy|]. intros _. now unfold cexp, fxy; simpl. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ