proposition: Theorem Znearest_half : forall x, (Rabs (x - IZR (Znearest x)) <= /2)%R.
proof: Proof. intros x. destruct (Req_dec (x - IZR (Zfloor x)) (/2)) as [Hx|Hx]. assert (K: (Rabs (/2) <= /2)%R). apply Req_le. apply Rabs_pos_eq. apply Rlt_le. apply Rinv_0_lt_compat. now apply IZR_lt. destruct (Znearest_DN_or_UP x) as [H|H] ; rewrite H ; clear H. now rewrite Hx. rewrite Zceil_floor_neq. rewrite plus_IZR. replace (x - (IZR (Zfloor x) + 1))%R with (x - IZR (Zfloor x) - 1)%R by ring. rewrite Hx. rewrite Rabs_minus_sym. now replace (1 - /2)%R with (/2)%R by field. apply Rlt_not_eq. apply Rplus_lt_reg_l with (- IZR (Zfloor x))%R. rewrite Rplus_opp_l, Rplus_comm. fold (x - IZR (Zfloor x))%R. rewrite Hx. apply Rinv_0_lt_compat. now apply IZR_lt. apply Rlt_le. now apply Znearest_N_strict. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop