It's easy to just figure out the values like you suggest and say yes, 1=1 so it is correct, but that's not a formal enough proof, it just tells us that it should be correct.
You can show the base cae is true, now suppose the invariant holds for some , if is odd then on the -st trip around the loop at the top of the loop .
Now at the end of the loop:
(note in the last line the value of used is that produced by the previous line not what it was at the top of the loop)
So the invariant holds in this case.
Now if is even, at the top of the look after the k-th itteration:
and at the end of the loop:
so the invariant holds in this case also, and so the given loop invariant is indeed a loop invariant for this loop.