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

State before:
⊢ 3 = succ (succ (succ zero))
Tactic:
rw [three_eq_succ_two]
State after:
⊢ succ 2 = succ (succ (succ zero))

State before:
⊢ succ 2 = succ (succ (succ zero))
Tactic:
rw [two_eq_succ_one]
State after:
⊢ succ (succ 1) = succ (succ (succ zero))

State before:
⊢ succ (succ 1) = succ (succ (succ zero))
Tactic:
rw [one_eq_succ_zero]
State after:
⊢ succ (succ (succ 0)) = succ (succ (succ zero))

State before:
⊢ succ (succ (succ 0)) = succ (succ (succ zero))
Tactic:
rw [zero_eq]
State after:
no goals