proposition: Lemma Rnearbyint_error_NE x : (- (1/2) <= Rnearbyint rnd_NE x - x <= 1/2)%R.
proof: Proof. simpl. assert (H := Znearest_half (fun x => negb (Z.even x)) x). split_Rabs; lra. Qed.
imports: Coq(Reals ZArith Psatz) Flocq(Core) Xreal