mathlib3 documentation

Divide linear combinations into three groups by the coefficient of the mth variable in their resultant terms: negative, zero, or positive.

Use two linear combinations to obtain a third linear combination whose resultant term does not include the mth variable.

Use two lists of linear combinations (one in which the resultant terms include occurrences of the mth variable with positive coefficients, and one with negative coefficients) and linearly combine them in every possible way that eliminates the mth variable.

Search through a list of (linear combination × resultant term) pairs, find the first pair whose resultant term has a negative constant term, and return its linear combination

First, eliminate all variables by Fourier–Motzkin elimination. When all variables have been eliminated, find and return the linear combination which produces a constraint of the form 0 < k + t such that k is the constant term of the RHS and k < 0.

Perform Fourier–Motzkin elimination to find a contradictory linear combination of input constraints.