proposition: Lemma Znearest_IZR c z : Znearest c (IZR z) = z.
proof: Proof. unfold Znearest; rewrite Zceil_IZR, Zfloor_IZR. now destruct Rcompare; try easy; destruct c. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic