proposition: Lemma Rnearbyint_IZR mode z : Rnearbyint mode (IZR z) = IZR z.
proof: Proof. now destruct mode; simpl; rewrite ?Zceil_IZR, ?Zfloor_IZR, ?Ztrunc_IZR, ?Znearest_IZR. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic