ASM_REAL_ARITH_TAC : tactic
# g `!x y z:real. abs(x) <= y ==> abs(x - z) <= abs(y + abs(z))`;; val it : goalstack = 1 subgoal (1 total) `!x y z. abs x <= y ==> abs (x - z) <= abs (y + abs z)` # e(REPEAT STRIP_TAC);; val it : goalstack = 1 subgoal (1 total) 0 [`abs x <= y`] `abs (x - z) <= abs (y + abs z)` # e REAL_ARITH_TAC;; Exception: Failure "linear_ineqs: no contradiction". # e ASM_REAL_ARITH_TAC;; val it : goalstack = No subgoals