Theorem: MyNat.pow_succ (NNG/MyNat/Power.lean)

State before:
m n : ℕ
⊢ m ^ succ n = m ^ n * m
Tactic:
rfl
State after:
no goals