Proof Obligation 2
Show
INV and k!=0 and odd(k) ==> P2
We do this again by examining each clause of P2 and seeing if its information is implied by the left side above ...
k-1 >= 0 is implied by (k>=0 and k!=0)
x!=0 and z!=0 are direct components of INV...
rewrite x^n = (y*z)*z^(k-1) so we have:
x^n = y*z^(k-1+1) = y*z^k, a component of INV
QED
