proposition: Theorem Ztrunc_abs : forall x, Ztrunc (Rabs x) = Z.abs (Ztrunc x).
proof: Proof. intros x. rewrite Ztrunc_floor. 2: apply Rabs_pos. unfold Ztrunc. case Rlt_bool_spec ; intro H. rewrite Rabs_left with (1 := H). rewrite Zabs_non_eq. apply sym_eq. apply Z.opp_involutive. apply Zceil_glb. now apply Rlt_le. rewrite Rabs_pos_eq with (1 := H). apply sym_eq. apply Z.abs_eq. now apply Zfloor_lub. Qed.
imports: Coq(Psatz Reals ZArith) Zaux