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