mathlib documentation

tactic.omega.nat.form

@[simp]

univ_close p n := p closed by prepending n universal quantifiers

Equations

Return expr of proof that argument is free of subtractions

Equations

All valuations satisfy argument

Equations

There exists some valuation that satisfies argument

Equations

implies p q := under any valuation, q holds if p holds

Equations

equiv p q := under any valuation, p holds iff q holds

Equations

There does not exist any valuation that satisfies argument

Equations
Equations

Tactic for setting up proof by induction over preforms.