proposition: Lemma ZnearestE_plus_even : forall x n, Z.even n = true -> (ZnearestE x + n = ZnearestE (x + IZR n))%Z.
proof: Proof. intros x n Hneven. unfold ZnearestE, Zceil. rewrite Ropp_plus_distr, <-opp_IZR, <-2Zfloor_add, plus_IZR. ring_simplify (x + IZR n - (IZR (Zfloor x) + IZR n)). rewrite Z.even_add_even by now apply Z.even_spec. case negb, Rcompare; ring. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)