proposition: Theorem round_UP_plus_eps : forall x, F x -> forall eps, (0 < eps <= if (Rle_bool 0 x) then (ulp x) else (ulp (pred (-x))))%R -> round beta fexp Zceil (x + eps) = (succ x)%R.
proof: Proof. Proof with auto with typeclass_instances. intros x Fx eps Heps. case (Rle_or_lt 0 x); intros Zx. rewrite succ_eq_pos; try assumption. rewrite Rle_bool_true in Heps; trivial. apply round_UP_plus_eps_pos; assumption. rewrite Rle_bool_false in Heps; trivial. rewrite <- (Ropp_involutive (x+eps)). rewrite <- (Ropp_involutive (succ x)). rewrite round_UP_opp. apply f_equal. replace (-(x+eps))%R with (-succ x + (-eps + ulp (pred (-x))))%R. apply round_DN_plus_eps_pos. rewrite <- pred_opp. apply pred_ge_0. now apply Ropp_0_gt_lt_contravar. now apply generic_format_opp. now apply generic_format_opp, generic_format_succ. split. apply Rplus_le_reg_l with eps; ring_simplify. apply Heps. unfold pred; rewrite Ropp_involutive. apply Rplus_lt_reg_l with (eps-ulp (- succ x))%R; ring_simplify. apply Heps. unfold succ; rewrite Rle_bool_false; try assumption. apply trans_eq with (-x +-eps)%R;[idtac|ring]. pattern (-x)%R at 3; rewrite <- (pred_pos_plus_ulp (-x)). rewrite pred_eq_pos. ring. left; now apply Ropp_0_gt_lt_contravar. now apply Ropp_0_gt_lt_contravar. now apply generic_format_opp. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop