proposition: Theorem OddExp : forall (n : Z) (m : nat), Odd n -> Odd (Zpower_nat n m).
proof: Proof. intros n m; elim m; simpl in |- *. intros; apply Odd1. intros n0 H H0; replace (S n0) with (1 + n0); auto with arith. apply OddMult; try easy. now apply H. Qed.
imports: Reals ZArith List PeanoNat Psatz