Proof Obligation 4
Show
P4 ==> POST
substitute k = 0 into x^n = y*z^k
get x^n = y
QED