ASM_ARITH_TAC : tactic
# g `1 <= 6 * x /\ 2 * x <= 3 ==> x = 1`;; Warning: Free variables in goal: x val it : goalstack = 1 subgoal (1 total) `1 <= 6 * x /\ 2 * x <= 3 ==> x = 1` # e STRIP_TAC;; val it : goalstack = 1 subgoal (1 total) 0 [`1 <= 6 * x`] 1 [`2 * x <= 3`] `x = 1` # e ARITH_TAC;; Exception: Failure "linear_ineqs: no contradiction". # e ASM_ARITH_TAC;; val it : goalstack = No subgoals