Theorem: MyNat.zero_pow_succ (TheoremProvingLean/inductive_types.lean)

State before:
n : Nat
⊢ zero ^ succ n = zero
Tactic:
rw [pow_succ, mul_zero]
State after:
no goals