rw [sexp, sexp, sexp, hi, ←mul_assoc', mul_assoc' m, mul_comm' _ m, ←mul_assoc', ←mul_assoc']
case hs
r m n : ↑N0
hi : exp (mul (m, n), r) = mul (exp (m, r), exp (n, r))
⊢ exp (mul (m, n), S r) = mul (exp (m, S r), exp (n, S r))
no goals