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

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

 { PRE: x > 3 }

    if ( x < 25 ) then x := 2 * x

 { POST: x >= 8 }