Is this an issue with the law of the excluded middle, or an issue with the proof? Part of a proof requiring you to prove that if $x^2$ is odd then $x$ is odd (given that $x \in \mathbb{N}$). It is my understanding that the contrapositive is used for this as follows.
$x=2n, n \in \mathbb{N}$
$\Rightarrow x^2 = 4n^2$
$\Rightarrow x^2$ is even
Then using the contrapositive:
$\Rightarrow \lnot Even(x^2) \rightarrow \lnot Even(x)$
Now the Law of the excluded middle:
$\Rightarrow Odd(x^2) \rightarrow Odd(x)$
So reasonably straight forward. However, my issue with this is whilst $x^2$ is even, it is even more strictly defined as a multiple of $4$. So in the contrapositive sense it doesn't feel right that it can be any even number. So what happens if that said number is 6? Not strictly divisible by 4 but still even. This is a bit difficult because this proof's conclusion is actually correct and any squared integer is either divible by 4 or odd. But that was found through exhaustion in a different way. Using the law of the excluded middle after saying that it wasn't just any even number seems spurious.
Could someone please clarify if I am right with reservation about this? If not, please explain (without just saying it is contrapositive, therefore). I feel like there should be a continuing connection between the definition of what type of even and what can be deduced from that.

Ignore the broader proof - do you agree with the assertion "If $x$ is divisible by $4$, then $x$ is even?" This is all that's going on. We're always allowed to "forget" information in a proof, and this has nothing to do with the excluded middle. When you conclude "$x^2$ is even," this in no way implies that you've concluded "$x^2$ is even and that's the most that can be said."
