Proof Example 2: Dealing with IF-THEN-ELSE in a Proof

Consider this program fragment (assume we are using all integers):

 { PRE: x0 = x and y0 = y }

    if (x > y) then y := x

               else x := y

 { POST: x = y = max(x0,y0) }