fix(tactic/linarith): fix bug in linarith (#17307)
I discovered this bug while porting linarith to mathlib4, and @digama0 minimised and identified the problem. There is a [zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/bug.20in.20linarith) explaining the details.
When applying [Imbert's first acceleration theorem](https://en.wikipedia.org/wiki/Fourier%E2%80%93Motzkin_elimination#Imbert's_acceleration_theorems) the code was incorrectly interpreting what an "implicitly eliminated variable" was.
I've added two tests, a one-liner that Mario reduced the problem too, as well as a longer one which had been failing in the mathlib4 port (due to different variable ordering).
The change causes one proof to timeout, which has been sped up.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
