Prove that power2 is strict. While one can base the proof on the "obvious" fact that power2 n is ${\displaystyle 2^{n}}$, the latter is preferably proven using fixed point iteration.