Theorem: Cpdt.Chapter4.add_IsZero (Cpdt/Chapter4/InductivePred.lean)

State before:
m n : Nat
⊢ IsZero m → n + m = n
Tactic:
intro h
State after:
m n : Nat
h : IsZero m
⊢ n + m = n

State before:
m n : Nat
h : IsZero m
⊢ n + m = n
Tactic:
cases h
State after:
case zero
n : Nat
⊢ n + 0 = n

State before:
case zero
n : Nat
⊢ n + 0 = n
Tactic:
rfl
State after:
no goals