specialize hi m n
case hs
r : ↑N0
hi : ∀ (m n : ↑N0), exp (exp (m, n), r) = exp (m, mul (n, r))
m n : ↑N0
⊢ exp (exp (m, n), S r) = exp (m, mul (n, S r))
case hs
r m n : ↑N0
hi : exp (exp (m, n), r) = exp (m, mul (n, r))
⊢ exp (exp (m, n), S r) = exp (m, mul (n, S r))