Complex.logTaylor_succ_neg

lemma logTaylor_succ_neg (n : ℕ) (z : ℂ) :    logTaylor (n + 1) (-z) = logTaylor n (-z) - z ^ n / n := by  rw [logTaylor_succ, Pi.add_apply]  have hsign : (-1 : ℂ) ^ (n + 1) * (-z) ^ n = -z ^ n := by    have hzpow : (-z) ^ n = (((-1 : ℂ) * z) ^ n) := by simp    rw [hzpow, mul_pow, ← mul_assoc, ← pow_add]    have hpow : (-1 : ℂ) ^ (n + 1 + n) = (-1 : ℂ) := by      rw [show n + 1 + n = 2 * n + 1 by omega, pow_add, pow_mul]      norm_num    rw [hpow]    ring  rw [show (-1 : ℂ) ^ (n + 1) * (-z) ^ n / n = -(z ^ n / n) by    rw [hsign]    ring]  abel