proposition: Lemma Rnearbyint_error_ZR_pos x : (0 <= x -> -1 <= Rnearbyint rnd_ZR x - x <= 0)%R.
proof: Proof. simpl; unfold Ztrunc. case Rlt_bool_spec; try lra. now intros; apply Rnearbyint_error_DN. Qed.
imports: Coq(Reals ZArith Psatz) Flocq(Core) Xreal