proposition: Theorem Ztrunc_ceil : forall x, (x <= 0)%R -> Ztrunc x = Zceil x.
proof: Proof. intros x Hx. unfold Ztrunc. case Rlt_bool_spec ; intro H. apply refl_equal. rewrite (Rle_antisym _ _ Hx H). rewrite Zceil_IZR. apply Zfloor_IZR. Qed.
imports: Coq(Psatz Reals ZArith) Zaux