Splits a list of goals into two and applies a list-tactic to each part
DESCRIPTION
For list-tactics ltac1 and ltac2, integer n and goal list gl,
the application SPLIT_LT n (ltac1, ltac2) gl
applies ltac1 to the first n goals in gl, and ltac2 to the remainder.
If n is negative, ltac1 is applied to the goals before the last -n,
and ltac2 to the last -n goals.
FAILURE
The application SPLIT_LT n (ltac1, ltac2) never fails,
but when applied to a goal list,
it fails if the index n is (in absolute value)
larger then the length of the list,
or if either of the list-tactics ltac1 and ltac2 fails.
EXAMPLE
To apply tactic tac1 to a goal, and then to apply tac2
to all resulting subgoals except the first, use