INT_ARITH : term -> thm
# INT_ARITH `!x y:int. x <= y + &1 ==> x + &2 < y + &4`;; val it : thm = |- !x y. x <= y + &1 ==> x + &2 < y + &4 # INT_ARITH `(x + y:int) pow 2 = x pow 2 + &2 * x * y + y pow 2`;; val it : thm = |- (x + y) pow 2 = x pow 2 + &2 * x * y + y pow 2