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