$a^n$ even implies $a$ even I've tried to prove that $(\forall a,n>0 \in \mathbb{N}),(a^n \text{ even} \implies a \text{ even})$, can someone tell me whether my proof is sound?
Lemma 1: $a \text{ even} \implies a^2 \text{ even}$
Lemma 2: $a \text{ odd} \implies a^2 \text{ odd}$
$$a^n \text{ even} \equiv a^{n-1}a \text{ even} \equiv (a^{n-1} \text{ odd} \land a \text{ even}) \lor (a^{n-1} \text{ even} \land a \text{ odd}) \lor (a^{n-1} \text{ even} \land a \text{ even})$$
by virtue of Lemma 1 (by construction) $(a \text{ even} \implies a^{n-1} \text{ even})$ and by the same argument, from Lemma 2, $(a \text{ odd} \implies a^{n-1} \text{ odd})$
whence, $(a^{n-1} \text{ odd} \land a \text{ even}) \equiv \text{False}$ and $(a^{n-1} \text{ even} \land a \text{ odd}) \equiv \text{False}$
therefore, we can write
$a^n \text{ even} \equiv F \lor F \lor (a^{n-1} \text{ even} \land a \text{ even}) \equiv (a^{n-1} \text{ even} \land a \text{ even})$
Since, $(\text{True} \equiv a^n \text{ even} \equiv (a^{n-1} \text{ even} \land a \text{ even})) \therefore a^{n-1} \text{ even and a even} \square$

Your proof is almost valid, but it is unfortunately circular, because you use the following lemma:
$$a \text{ is odd} \implies a^{n-1} \text{ is odd}$$
However, if you take the contrapositive of this statement:
$$a^{n-1} \text{ is even} \implies a \text{ is even}$$
which is basically the same as your statement, except with $n-1$ instead of $n$.
Therefore, in order to make your proof valid, you need to pose it as a proof by induction, making $n=1$ your base case and then using the proof you have written above to show that $a^{n-1} \text{ is even} \implies a \text{ is even}$ can be used to prove $a^n \text{ is even} \implies a \text{ is even}$.
