Theorem: LO.Nat.numeral_eq (Logic/FirstOrder/Arith/Basic.lean)

State before:
n : ℕ
⊢ ORingSymbol.numeral (n + 2) = n + 2
Tactic:
simp[ORingSymbol.numeral, Nat.numeral_eq (n + 1)]
State after:
no goals