mathlib documentation

tactic.​omega.​nat.​sub_elim

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

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