Theorem: Int.pow_succ (MLIR/Util/Arith.lean)

State before:
n : ℤ
m : ℕ
⊢ n ^ (m + 1) = n ^ m * n
Tactic:
rfl
State after:
no goals