ARITH_RULE : term -> thm
# ARITH_RULE `x = 1 ==> y <= 1 \/ x < y`;; val it : thm = |- x = 1 ==> y <= 1 \/ x < y # ARITH_RULE `x <= 127 ==> ((86 * x) DIV 256 = x DIV 3)`;; val it : thm = |- x <= 127 ==> (86 * x) DIV 256 = x DIV 3 # ARITH_RULE `2 * a * b EXP 2 <= b * a * b ==> (SUC c - SUC(a * b * b) <= c)`;; val it : thm = |- 2 * a * b EXP 2 <= b * a * b ==> SUC c - SUC (a * b * b) <= c