The fact that [Fourier-Motzkin elimination][1] gives a sound and complete procedure for determining whether a system of linear inequalities has a solution (and for computing the existential projection of the solution-set onto a subset of the variables). The proof is intuitive, very difficult to forget, and provides a useful procedure for hand-computations in low dimensions. [Farkas' Lemma][2] follows as an obvious consequence.

The general idea of variable elimination occurs throughout mathematics and logic and is closely connected to tools used to automate mathematics - for instance, the Resolution proof system is used in SAT-solving, for algebraic geometry we use Gröbner bases, for polynomial inequalities we use Cylindrical Algebraic Decomposition. Fourier-Motzkin elimination is a perfect introduction to the general technique and is often practically useful. Farkas' Lemma also motivates convex duality, a cornerstone of mathematical optimization.


  [1]: https://en.wikipedia.org/wiki/Fourier%E2%80%93Motzkin_elimination
  [2]: https://en.wikipedia.org/wiki/Farkas%27_lemma