proposition: Theorem EvenExp : forall (n : Z) (m : nat), Even n -> Even (Zpower_nat n (S m)).
proof: Proof. intros n m; elim m. rewrite Zpower_nat_1; simpl in |- *; auto with zarith. intros n0 H H0; replace (S (S n0)) with (1 + S n0); auto with arith. rewrite Zpower_nat_is_exp; rewrite Zpower_nat_1; simpl in |- *; auto with zarith. now apply EvenMult1. Qed.
imports: Reals ZArith List PeanoNat Psatz