fact: Definition Znearest x := match Rcompare (x - IZR (Zfloor x)) (/2) with | Lt => Zfloor x | Eq => if choice (Zfloor x) then Zceil x else Zfloor x | Gt => Zceil x end.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop