proposition: Lemma Rnearbyint_error_UP x : (0 <= Rnearbyint rnd_UP x - x <= 1)%R.
proof: Proof. assert (H := (Zfloor_ub (- x), Zfloor_lb (- x))). simpl; unfold Zceil; rewrite opp_IZR. case H; simpl; lra. Qed.
imports: Coq(Reals ZArith Psatz) Flocq(Core) Xreal