fun max(x,y) {
  if x >= y { x } else { y }
}
fun min(x,y) {
  if x >= y { y } else { x }
}
max(1,1) == 1
max(1,2) == 2
max(2,1) == 2
min(1,1) == 1
min(1,2) == 1
min(2,1) == 1
//forall(x) x:uint ==> max(x,x) == x
//forall(x) x:uint ==> min(x,x) == x
//forall(x) x:uint ==> min(x,x+1) == x
//forall(x,y) (x:uint && y:uint) ==> max(x,y) >= x
//forall(x,y) (x:uint && y:uint) ==> max(x,y) >= y
//forall(x,y) (x:uint && y:uint) ==> max(x,y) >= min(x,y)