# mathlibdocumentation

tactic.omega.find_scalars

meta def omega.trisect (m : ) :

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

meta def omega.elim_var_aux (m : ) :

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

meta def omega.elim_var (m : ) (neg pos : list ) :

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.

meta def omega.find_neg_const  :

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

meta def omega.find_scalars_core  :
list tactic (list )

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.