proposition: Theorem round_plus_ge_ulp : forall x y, format x -> format y -> round beta fexp rnd (x+y) <> 0%R -> (ulp beta fexp (x/IZR beta) <= Rabs (round beta fexp rnd (x+y)))%R.
proof: Proof. Proof with auto with typeclass_instances. intros x y Fx Fy KK. case (Req_dec x 0); intros Zx. rewrite Zx, Rplus_0_l. rewrite round_generic... unfold Rdiv; rewrite Rmult_0_l. rewrite Fy. unfold F2R; simpl; rewrite Rabs_mult. rewrite (Rabs_pos_eq (bpow _)) by apply bpow_ge_0. case (Z.eq_dec (Ztrunc (scaled_mantissa beta fexp y)) 0); intros Hm. contradict KK. rewrite Zx, Fy, Hm; unfold F2R; simpl. rewrite Rplus_0_l, Rmult_0_l. apply round_0... apply Rle_trans with (1*bpow (cexp y))%R. rewrite Rmult_1_l. rewrite <- ulp_neq_0. apply ulp_ge_ulp_0... intros K; apply Hm. rewrite K, scaled_mantissa_0. apply Ztrunc_IZR. apply Rmult_le_compat_r. apply bpow_ge_0. rewrite <- abs_IZR. apply IZR_le. apply (Zlt_le_succ 0). now apply Z.abs_pos. destruct (round_plus_F2R x y Fx Fy Zx) as (m,Hm). case (Z.eq_dec m 0); intros Zm. contradict KK. rewrite Hm, Zm. apply F2R_0. rewrite Hm, <- F2R_Zabs. rewrite ulp_neq_0. rewrite <- (Rmult_1_l (bpow _)). apply Rmult_le_compat_r. apply bpow_ge_0. apply IZR_le. apply (Zlt_le_succ 0). now apply Z.abs_pos. apply Rmult_integral_contrapositive_currified with (1 := Zx). apply Rinv_neq_0_compat. apply Rgt_not_eq, radix_pos. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative