program correctness of an if-then wff

The problem I have is:

{True} if x > y then x := y + 1; y := x + 1 fi {x ≤ y}

I have solved some If statements, but I have never done one where it has the "fi" at the end. I am told that the solution requires us to prove the two statements:

1. {True ∧ (x > y)} x := y + 1; y := x + 1{x ≤ y}
2. True ∧ (x ≤ y) → (x ≤ y)

which I'm not sure how to go about doing. I've gotten to where I show one of the statements, but after that I'm not sure where to go. Any ideas? Thanks.

I posted this in the Math.stackexchange page, but all of them seemed to say that this was not a math question that this is more of a programming/CS question and that I was asking this in the wrong place, so I thought I'd try it here.