rw [pow_succ, pow_succ, pow_succ, ih]
case succ
k' : ℕ
ih : 10 ^ k' = 2 ^ k' * 5 ^ k'
⊢ 10 ^ (k' + 1) = 2 ^ (k' + 1) * 5 ^ (k' + 1)
case succ
k' : ℕ
ih : 10 ^ k' = 2 ^ k' * 5 ^ k'
⊢ 2 ^ k' * 5 ^ k' * 10 = 2 ^ k' * 2 * (5 ^ k' * 5)