Proof Obligation 4

Show

    P4 ==> POST

• substitute k = 0 into x^n = y*z^k
• get x^n = y

QED