Tactic for proving arithmetic goals needing basic rearrangement and linear
inequality reasoning only.
DESCRIPTION
ARITH_TAC will automatically prove goals that require basic algebraic
normalization and inequality reasoning over the natural numbers. For nonlinear
equational reasoning use NUM_RING and derivatives.
FAILURE CONDITIONS
Fails if the automated methods do not suffice.
EXAMPLE
# g `1 <= x /\ x <= 3 ==> x = 1 \/ x = 2 \/ x = 3`;;
Warning: Free variables in goal: x
val it : goalstack = 1 subgoal (1 total)
`1 <= x /\ x <= 3 ==> x = 1 \/ x = 2 \/ x = 3`
# e ARITH_TAC;;
val it : goalstack = No subgoals