Theorem: Nat.zero_pow_succ (GMLInit/Data/Nat/Pow.lean)

State before:
x : Nat
⊢ 0 ^ (x + 1) = 0 ^ x * 0
Tactic:
rw [Nat.pow_succ]
State after:
no goals

State before:
x : Nat
⊢ 0 ^ x * 0 = 0
Tactic:
rw [Nat.mul_zero]
State after:
no goals