Prove the correctness of the iterative program "subtract_two_integers"

Pre-condition: x, y belong to the integers and y > 0

Post-condition: returns x - y

Subtract_two_integers(x, y):

while y > 0:

x = x - 1

y = y - 1

return x

What is the loop invariant? How does the loop terminate? and how do i show the loop invariant holds after the exit condition?

Can you please show all that in the proof of correctness of this program.