proposition: Theorem Zaway_abs : forall x, Zaway (Rabs x) = Z.abs (Zaway x).
proof: Proof. intros x. rewrite Zaway_ceil. 2: apply Rabs_pos. unfold Zaway. case Rlt_bool_spec ; intro H. rewrite Rabs_left with (1 := H). rewrite Zabs_non_eq. apply (f_equal (fun v => - Zfloor v)%Z). apply Ropp_involutive. apply le_IZR. apply Rlt_le. apply Rle_lt_trans with (2 := H). apply Zfloor_lb. rewrite Rabs_pos_eq with (1 := H). apply sym_eq. apply Z.abs_eq. apply le_IZR. apply Rle_trans with (1 := H). apply Zceil_ub. Qed.
imports: Coq(Psatz Reals ZArith) Zaux