advice on pen+paper maths proof before I create a lean proof

Stream: new members

[rzeta0]

I'm doing the MoP Exercise on strong induction - there is only one exercise for that section, ex 6.4.3:

Show that for all natural numbers $n>0$ , there exist natural numbers  $a$ and $$$x$, with  $x$ odd, such that $n=2^{a}x$.

Start with a case split on the parity of $n$, using the lemma even_or_odd.

I wanted to check that my pen-n-paper maths strategy was correct before I try writing the code:

• for $n$ odd we need to show there exists $a$ and odd $x$ such that $2^{a}x$. This only works if $a=0$ otherwise $2^{a}x$ is always even. For the "there exists" we can choose $x=n$ since n is odd.
• There is no need for induction for the above first case ?!
• for $n$ even we need to show there exists $a$ and odd $x$ such that $[2^{a}x]$. We can't have $a=0$ because $x$ is odd and we need $2^{a}x=x$ to be even, but $x$ is odd. We can use $a=2$ and choose $x=n$, which works.
• Again there was no need for induction for this second case ?!

Clearly I must be deeply in error somewhere?

[Edward van de Meent]

if $n$ is even, choosing $a = 2$ and $x = n$ results in you needing to prove that $n = 2 ^ a x = 2 ^ 2 n = 4 n$. This is false, so the choices are wrong.

[Ruben Van de Velde]

And if $n$ is even, you can't set $x$ to be $n$ anyway, because $x$ has to be odd

[Ruben Van de Velde]

Your argument for $n$ odd is correct, though

[rzeta0]

silly me !

[Ruben Van de Velde]

Maybe it helps to take an example - say $n = 12$, what are the values for $x$ and $a$?

[Edward van de Meent]

(spoiler, these are unique)