dos cosas

uno:

The previous post was incorrect. The loop invariant did not, in fact, remain unchanged. Though the loop invariant as it were was correct, it was not helpful in proving the post condition.  I struggled to derive what would be the new invariant, but after excessive trial and error I realized that I was going to have to rely on the loop invariant to prove the postcondition, so looking at the postcondition should have been my first step in trying to determine one.

and so I did!

which leads me to.....

dos:

I SUCCESSFULLY PROVED MY FIRST PROGRAM.

yeyeyeyeyeye

Virtual high fives all around. (y)