If prf is a proof of ¬ e, where e is a comparison, rem_neg prf e flips the comparison in e and returns a proof. For example, if prf : ¬ a < b, rem_neg prf `(a < b) returns a proof of a ≥ b.

rearr_comp e takes a proof e of an equality, inequality, or negation thereof, and turns it into a proof of a comparison _ R 0, where R ∈ {=, ≤, <}.

If e is of the form ((n : ℕ) : ℤ), is_nat_int_coe e returns n : ℕ.

If e : ℕ, returns a proof of 0 ≤ (e : ℤ).

get_nat_comps e returns a list of all subexpressions of e of the form ((t : ℕ) : ℤ).

If pf is a proof of a strict inequality (a : ℤ) < b, mk_non_strict_int_pf_of_strict_int_pf pf returns a proof of a + 1 ≤ b, and similarly if pf proves a negated weak inequality.

is_nat_prop tp is true iff tp is an inequality or equality between natural numbers or the negation thereof.

is_strict_int_prop tp is true iff tp is a strict inequality between integers or the negation of a weak inequality between integers.

Removes any expressions that are not proofs of inequalities, equalities, or negations thereof.

Replaces proofs of negations of comparisons with proofs of the reversed comparisons. For example, a proof of ¬ a < b will become a proof of a ≥ b.

If h is an equality or inequality between natural numbers, nat_to_int lifts this inequality to the integers. It also adds the facts that the integers involved are nonnegative. To avoid adding the same nonnegativity facts many times, it is a global preprocessor.

strengthen_strict_int h turns a proof h of a strict integer inequality t1 < t2 into a proof of t1 ≤ t2 + 1.

mk_comp_with_zero h takes a proof h of an equality, inequality, or negation thereof, and turns it into a proof of a comparison _ R 0, where R ∈ {=, ≤, <}.

normalize_denominators_in_lhs h lhs assumes that h is a proof of lhs R 0. It creates a proof of lhs' R 0, where all numeric division in lhs has been cancelled.

cancel_denoms pf assumes pf is a proof of t R 0. If t contains the division symbol /, it tries to scale t to cancel out division by numerals.

find_squares m e collects all terms of the form a ^ 2 and a * a that appear in e and adds them to the set m. A pair (a, tt) is added to m when a^2 appears in e, and (a, ff) is added to m when a*a appears in e.

nlinarith_extras is the preprocessor corresponding to the nlinarith tactic.

• For every term t such that t^2 or t*t appears in the input, adds a proof of t^2 ≥ 0 or t*t ≥ 0.
• For every pair of comparisons t1 R1 0 and t2 R2 0, adds a proof of t1*t2 R 0.

This preprocessor is typically run last, after all inputs have been canonized.

remove_ne_aux case splits on any proof h : a ≠ b in the input, turning it into a < b ∨ a > b. This produces 2^n branches when there are n such hypotheses in the input.

remove_ne case splits on any proof h : a ≠ b in the input, turning it into a < b ∨ a > b, by calling linarith.remove_ne_aux. This produces 2^n branches when there are n such hypotheses in the input.

The default list of preprocessors, in the order they should typically run.

preprocess pps l takes a list l of proofs of propositions. It maps each preprocessor pp ∈ pps over this list. The preprocessors are run sequentially: each recieves the output of the previous one. Note that a preprocessor may produce multiple or no expressions from each input expression, so the size of the list may change.