INT_ARITH_TAC : tactic
# prioritize_int();; val it : unit = () # g `(x1 pow 2 + x2 pow 2 + x3 pow 2 + x4 pow 2) * (y1 pow 2 + y2 pow 2 + y3 pow 2 + y4 pow 2) = (x1 * y1 - x2 * y2 - x3 * y3 - x4 * y4) pow 2 + (x1 * y2 + x2 * y1 + x3 * y4 - x4 * y3) pow 2 + (x1 * y3 - x2 * y4 + x3 * y1 + x4 * y2) pow 2 + (x1 * y4 + x2 * y3 - x3 * y2 + x4 * y1) pow 2`;;
# g `!x y:int. abs(x + y) < abs(x) + abs(y) + &1`;;
# e INT_ARITH_TAC;; val it : goalstack = No subgoals