Theorem: LeanDemo.three_eq_succ_succ_succ_zero' (LeanMeetup/Demo01.lean)

State before:
⊢ 3 = succ (succ (succ zero))
Tactic:
rw [three_eq_succ_two, two_eq_succ_one, one_eq_succ_zero, zero_eq]
State after:
no goals