The proof, given above, is probably more detailed than really needed. However, the way the proof is given may be of some interest, as it illustrates reasoning with invariants in a hopefully somewhat illuminating way.
See the last page for a few comments and links.