pub open spec fn min(x: int, y: int) -> int
{ if x <= y { x } else { y } }
This function computes the minimum of two given integers.