proposition: Theorem round_UP_pred_plus_eps : forall x, F x -> forall eps, (0 < eps <= if Rle_bool x 0 then ulp x else ulp (pred x))%R -> round beta fexp Zceil (pred x + eps) = x.
proof: Proof. intros x Fx eps Heps. rewrite round_UP_plus_eps. now apply succ_pred. now apply generic_format_pred. unfold pred at 4. rewrite Ropp_involutive, pred_succ. rewrite ulp_opp. generalize Heps; case (Rle_bool_spec x 0); intros H1 H2. rewrite Rle_bool_false; trivial. case H1; intros H1'. apply Rlt_le_trans with (2:=H1). apply pred_lt_id. now apply Rlt_not_eq. rewrite H1'; unfold pred, succ. rewrite Ropp_0; rewrite Rle_bool_true;[idtac|now right]. rewrite Rplus_0_l. rewrite <- Ropp_0; apply Ropp_lt_contravar. apply Rlt_le_trans with (1:=proj1 H2). apply Rle_trans with (1:=proj2 H2). rewrite Ropp_0, H1'. now right. rewrite Rle_bool_true; trivial. now apply pred_ge_0. now apply generic_format_opp. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop