Proof of function to normalize angles using why3

Problem: Write a function to normalize an angle to between -179 and 180 degrees (inclusive).

Solution (as found on StackOverflow here: https://stackoverflow.com/questions/2320986/easy-way-to-keeping-angles-between-179-and-180-degrees/2323034#2323034):

// reduce the angle  
angle =  angle % 360; 

// force it to be the positive remainder, so that 0 <= angle < 360  
angle = (angle + 360) % 360;  

// force into the minimum absolute value residue class, so that -180 < angle <= 180  
if (angle > 180)  
    angle -= 360; 

Proof (verify on http://why3.lri.fr/try/):

module NormalizeAngle

  use int.Int 
  use int.ComputerDivision

  let normalize (a: int) : int
    requires { true }
    ensures  { result > -180 /\ result <= 180 /\ mod (a - result) 360 = 0 }
  =
    let ref r = a in
    r <- mod r 360;
    r <- mod (r + 360) 360;
    if r > 180 then r <- r - 360;
    r

  let main () =
    normalize (270)

end

This proof proves that the return value from the function is indeed between -179 and 180 and furthermore that the result is congruent to the input modulo 360 (recall that a and b are congruent mod n if their difference is divisible by n), which means that they are equal.