Theorem: plusR_zero_left (Fpil/Chap09/Sec00.lean)

State before:
k : Nat
⊢ k = Nat.plusR 0 k
Tactic:
induction k with
| zero => rfl
| succ n ih =>
  unfold Nat.plusR
  rw [←ih]
State after:
no goals

State before:
case zero

⊢ Nat.zero = Nat.plusR 0 Nat.zero
Tactic:
rfl
State after:
no goals

State before:
case succ
n : Nat
ih : n = Nat.plusR 0 n
⊢ Nat.succ n = Nat.plusR 0 (Nat.succ n)
Tactic:
unfold Nat.plusR
State after:
case succ
n : Nat
ih : n = Nat.plusR 0 n
⊢ Nat.succ n = Nat.plusR 0 n + 1

State before:
case succ
n : Nat
ih : n = Nat.plusR 0 n
⊢ Nat.succ n = Nat.plusR 0 n + 1
Tactic:
rw [←ih]
State after:
no goals