proposition: Theorem Zceil_ub : forall x : R, (x <= IZR (Zceil x))%R.
proof: Proof. intros x. unfold Zceil. rewrite opp_IZR. apply Ropp_le_cancel. rewrite Ropp_involutive. apply Zfloor_lb. Qed.
imports: Coq(Psatz Reals ZArith) Zaux