proposition: Theorem Ztrunc_le : forall x y, (x <= y)%R -> (Ztrunc x <= Ztrunc y)%Z.
proof: Proof. intros x y Hxy. unfold Ztrunc at 1. case Rlt_bool_spec ; intro Hx. unfold Ztrunc. case Rlt_bool_spec ; intro Hy. now apply Zceil_le. apply Z.le_trans with 0%Z. apply Zceil_glb. now apply Rlt_le. now apply Zfloor_lub. rewrite Ztrunc_floor. now apply Zfloor_le. now apply Rle_trans with x. Qed.
imports: Coq(Psatz Reals ZArith) Zaux