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

State before:
k : Nat
⊢ k = Nat.plusR 0 k
Tactic:
induction k <;> simp [Nat.plusR] <;> assumption
State after:
no goals