proposition: Theorem generic_format_plus_weak : forall x y, format x -> format y -> (Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R -> format (x + y)%R.
proof: Proof. intros x y Fx Fy Hxy. destruct (Req_dec x R0) as [Zx|Zx]. now rewrite Zx, Rplus_0_l. destruct (Req_dec y R0) as [Zy|Zy]. now rewrite Zy, Rplus_0_r. apply generic_format_plus ; try assumption. apply Rle_trans with (1 := Hxy). unfold Rmin. destruct (Rle_dec (Rabs x) (Rabs y)) as [Hxy'|Hxy']. rewrite Z.min_l. destruct (mag beta x) as (ex, Hx). apply Rlt_le; now apply Hx. now apply mag_le_abs. rewrite Z.min_r. destruct (mag beta y) as (ex, Hy). apply Rlt_le; now apply Hy. apply mag_le_abs. exact Zy. apply Rlt_le. now apply Rnot_le_lt. Qed.
imports: Coq(ZArith Reals) Zaux Raux Defs Generic_fmt Operations