Theorem: nat_succ_eq_plus_one (Katydid/Std/Lists.lean)

State before:
n : ℕ
⊢ succ n = n + 1
Tactic:
simp only
State after:
no goals