(rw [pow_succ])
case succ
a b n' : Nat
ih : (a * b) ^ n' = a ^ n' * b ^ n'
⊢ a ^ n' * b ^ n' * (a * b) = a ^ n' * a * b ^ succ n'
case succ
a b n' : Nat
ih : (a * b) ^ n' = a ^ n' * b ^ n'
⊢ a ^ n' * b ^ n' * (a * b) = a ^ n' * a * (b ^ n' * b)