proposition: Theorem Zrnd_DN_or_UP : forall x, rnd x = Zfloor x \/ rnd x = Zceil x.
proof: Proof. intros x. destruct (Zle_or_lt (rnd x) (Zfloor x)) as [Hx|Hx]. left. apply Zle_antisym with (1 := Hx). rewrite <- (Zrnd_IZR (Zfloor x)). apply Zrnd_le. apply Zfloor_lb. right. apply Zle_antisym. rewrite <- (Zrnd_IZR (Zceil x)). apply Zrnd_le. apply Zceil_ub. rewrite Zceil_floor_neq. lia. intros H. rewrite <- H in Hx. rewrite Zfloor_IZR, Zrnd_IZR in Hx. apply Z.lt_irrefl with (1 := Hx). Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop