proposition: Theorem pred_UP_le_DN : forall x, (pred (round beta fexp Zceil x) <= round beta fexp Zfloor x)%R.
proof: Proof. Proof with auto with typeclass_instances. intros x. destruct (generic_format_EM beta fexp x) as [Fx|Fx]. rewrite !round_generic... apply pred_le_id. case (Req_dec (round beta fexp Zceil x) 0); intros Zx. rewrite Zx; unfold pred; rewrite Ropp_0. unfold succ; rewrite Rle_bool_true;[idtac|now right]. rewrite Rplus_0_l; unfold ulp; rewrite Req_bool_true; trivial. case negligible_exp_spec'. intros (H1,H2). contradict Zx; apply round_neq_0_negligible_exp... intros L; apply Fx; rewrite L; apply generic_format_0. intros (n,(H1,Hn)); rewrite H1. case (Rle_or_lt (- bpow (fexp n)) (round beta fexp Zfloor x)); trivial; intros K. absurd (round beta fexp Zceil x <= - bpow (fexp n))%R. apply Rlt_not_le. rewrite Zx, <- Ropp_0. apply Ropp_lt_contravar, bpow_gt_0. apply round_UP_le_DN_lt; try assumption. apply generic_format_opp, generic_format_bpow. now apply valid_exp. assert (let u := round beta fexp Zceil x in pred u < u)%R as Hup. now apply pred_lt_id. apply round_DN_ge_UP_gt... apply generic_format_pred... now apply round_UP_pt. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop