proposition: Lemma Zeven_abs: forall z, Z.even (Z.abs z) = Z.even z.
proof: Proof. intros z; case (Zle_or_lt z 0); intros H1. rewrite Z.abs_neq; try assumption. apply Z.even_opp. rewrite Z.abs_eq; auto with zarith. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations