proposition: Lemma Rnearbyint_error m x : (-1 <= Rnearbyint m x - x <= 1)%R.
proof: Proof. assert (H1 := Rnearbyint_error_DN x). assert (H2 := Rnearbyint_error_UP x). assert (H3 := Rnearbyint_error_ZR x). assert (H4 := Rnearbyint_error_NE x). case m; lra. Qed.
imports: Coq(Reals ZArith Psatz) Flocq(Core) Xreal