proposition: Theorem Ztrunc_opp : forall x, Ztrunc (- x) = Z.opp (Ztrunc x).
proof: Proof. intros x. unfold Ztrunc at 2. case Rlt_bool_spec ; intros Hx. rewrite Ztrunc_floor. apply sym_eq. apply Z.opp_involutive. rewrite <- Ropp_0. apply Ropp_le_contravar. now apply Rlt_le. rewrite Ztrunc_ceil. unfold Zceil. now rewrite Ropp_involutive. rewrite <- Ropp_0. now apply Ropp_le_contravar. Qed.
imports: Coq(Psatz Reals ZArith) Zaux