proposition: Theorem Znearest_N_strict : forall x, (x - IZR (Zfloor x) <> /2)%R -> (Rabs (x - IZR (Znearest x)) < /2)%R.
proof: Proof. intros x Hx. unfold Znearest. case Rcompare_spec ; intros H. rewrite Rabs_pos_eq. exact H. apply Rle_0_minus. apply Zfloor_lb. now elim Hx. rewrite Rabs_left1. rewrite Ropp_minus_distr. rewrite Zceil_floor_neq. rewrite plus_IZR. apply Ropp_lt_cancel. apply Rplus_lt_reg_l with 1%R. replace (1 + -/2)%R with (/2)%R by field. now replace (1 + - (IZR (Zfloor x) + 1 - x))%R with (x - IZR (Zfloor x))%R by ring. apply Rlt_not_eq. apply Rplus_lt_reg_l with (- IZR (Zfloor x))%R. apply Rlt_trans with (/2)%R. rewrite Rplus_opp_l. apply Rinv_0_lt_compat. now apply IZR_lt. now rewrite <- (Rplus_comm x). apply Rle_minus. apply Zceil_ub. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop