mathlib documentation

tactic.omega.nat.sub_elim

Find subtraction inside preterm and return its operands

Equations

Find (t - s) inside a preterm and replace it with variable k

Equations

Find subtraction inside preform and return its operands

Equations

Preform which asserts that the value of variable k is the truncated difference between preterms t and s

Equations

Return de Brujin index of fresh variable that does not occur in any of the arguments

Equations

Return a new preform with all subtractions eliminated

Equations