Proof Obligation 3
Show
INV and k!=0 ==> P3
which in this case is trivial, due to our if-then-else construction.
QED