REAL_ARITH_TAC : tactic
# g `(x1 pow 2 + x2 pow 2 + x3 pow 2 + x4 pow 2) pow 2 = ((x1 + x2) pow 4 + (x1 + x3) pow 4 + (x1 + x4) pow 4 + (x2 + x3) pow 4 + (x2 + x4) pow 4 + (x3 + x4) pow 4 + (x1 - x2) pow 4 + (x1 - x3) pow 4 + (x1 - x4) pow 4 + (x2 - x3) pow 4 + (x2 - x4) pow 4 + (x3 - x4) pow 4) / &6`;;
# g `&26 < x / &2 ==> abs(x / &4 + &1) < abs(x / &3)`;;
# e REAL_ARITH_TAC;; val it : goalstack = No subgoals