proposition: Lemma Zceil_plus: forall (n:Z) y, (Zceil (IZR n+y) = n + Zceil y)%Z.
proof: Proof. intros n y; unfold Zceil. rewrite Ropp_plus_distr, <- Ropp_Ropp_IZR. rewrite Zfloor_plus. ring. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations