mathlib3 documentation

tactic.omega.nat.sub_elim

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

Equations

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

Equations

Helper function for sub_elim

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