proposition: Theorem Znearest_DN_or_UP : forall x, Znearest x = Zfloor x \/ Znearest x = Zceil x.
proof: Proof. intros x. unfold Znearest. case Rcompare_spec ; intros _. now left. case choice. now right. now left. now right. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop