proposition: Theorem mag_plus_eps : forall x, (0 < x)%R -> F x -> forall eps, (0 <= eps < ulp x)%R -> mag beta (x + eps) = mag beta x :> Z.
proof: Proof. intros x Zx Fx eps Heps. destruct (mag beta x) as (ex, He). simpl. specialize (He (Rgt_not_eq _ _ Zx)). apply mag_unique. rewrite Rabs_pos_eq. rewrite Rabs_pos_eq in He. split. apply Rle_trans with (1 := proj1 He). pattern x at 1 ; rewrite <- Rplus_0_r. now apply Rplus_le_compat_l. apply Rlt_le_trans with (x + ulp x)%R. now apply Rplus_lt_compat_l. pattern x at 1 ; rewrite Fx. rewrite ulp_neq_0. unfold F2R. simpl. pattern (bpow (cexp beta fexp x)) at 2 ; rewrite <- Rmult_1_l. rewrite <- Rmult_plus_distr_r. rewrite <- plus_IZR. apply F2R_p1_le_bpow. apply gt_0_F2R with beta (cexp beta fexp x). now rewrite <- Fx. now rewrite <- Fx. now apply Rgt_not_eq. now apply Rlt_le. apply Rplus_le_le_0_compat. now apply Rlt_le. apply Heps. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop