proposition: Theorem Zceil_imp : forall n x, (IZR (n - 1) < x <= IZR n)%R -> Zceil x = n.
proof: Proof. intros n x Hnx. unfold Zceil. rewrite <- (Z.opp_involutive n). apply f_equal. apply Zfloor_imp. split. rewrite opp_IZR. now apply Ropp_le_contravar. rewrite <- (Z.opp_involutive 1). rewrite <- Zopp_plus_distr. rewrite opp_IZR. now apply Ropp_lt_contravar. Qed.
imports: Coq(Psatz Reals ZArith) Zaux