proposition: Theorem Znearest_imp : forall x n, (Rabs (x - IZR n) < /2)%R -> Znearest x = n.
proof: Proof. intros x n Hd. cut (Z.abs (Znearest x - n) < 1)%Z. clear ; lia. apply lt_IZR. rewrite abs_IZR, minus_IZR. replace (IZR (Znearest x) - IZR n)%R with (- (x - IZR (Znearest x)) + (x - IZR n))%R by ring. apply Rle_lt_trans with (1 := Rabs_triang _ _). simpl. replace 1%R with (/2 + /2)%R by field. apply Rplus_le_lt_compat with (2 := Hd). rewrite Rabs_Ropp. apply Znearest_half. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop