ASM_INT_ARITH_TAC : tactic
# g `!x y:int. x <= y /\ &2 * y <= &2 * x + &1 ==> x = y`;; val it : goalstack = 1 subgoal (1 total) `!x y. x <= y /\ &2 * y <= &2 * x + &1 ==> x = y` # e(REPEAT STRIP_TAC);; val it : goalstack = 1 subgoal (1 total) 0 [`x <= y`] 1 [`&2 * y <= &2 * x + &1`] `x = y` # e INT_ARITH_TAC;; Exception: Failure "linear_ineqs: no contradiction". # e ASM_INT_ARITH_TAC;; val it : goalstack = No subgoals