Finding a good loop invariant for a powering procedure
No, you can't say that $power \leq x^n$ is a loop invariant, since it is not maintained by the loop. For example, if $x &gt; 1$ and at the current iteration $power = x^n$, then the invariant is satisfied at the beginning of the loop but not at the end of the loop.

Also, this loop invariant doesn't help you prove that at the end $power = x^n$, which is presumably your end goal.

Try to think of an invariant which describes the value of $power$ in terms of $x$ and $i$.