proposition: Theorem round_UP_pred_plus_eps_pos : forall x, (0 < x)%R -> F x -> forall eps, (0 < eps <= ulp (pred x) )%R -> round beta fexp Zceil (pred x + eps) = x.
proof: Proof. intros x Hx Fx eps Heps. rewrite round_UP_plus_eps_pos; trivial. rewrite pred_eq_pos. apply pred_pos_plus_ulp; trivial. now left. now apply pred_ge_0. apply generic_format_pred; trivial. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop