Complex.logGammaSeq_succ_sub

lemma logGammaSeq_succ_sub {z : ℂ} (hz : 0 < z.re) (n : ℕ) :    logGammaSeq z (n + 1) - logGammaSeq z n      = z * ((Real.log ((n : ℝ) + 1) - Real.log n : ℝ) : ℂ) - log (1 + z / ((n : ℂ) + 1)) := by  have hn1 : (0 : ℝ) < (n : ℝ) + 1 := by positivity  have hnC : ((n : ℂ) + 1) ≠ 0 := Nat.cast_add_one_ne_zero n  have hx : 1 + z / ((n : ℂ) + 1) ≠ 0 := by    intro h    have hzval : z = -((n : ℂ) + 1) := by      field_simp at h      linear_combination h    rw [hzval] at hz    simp only [neg_re, add_re, natCast_re, one_re] at hz    have : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n    linarith  have hfacC : (Real.log ((n + 1)!) : ℂ)      = (Real.log ((n : ℝ) + 1) : ℂ) + (Real.log (n !) : ℂ) := by    have hfac : Real.log (((n + 1)! : ℕ) : ℝ)        = Real.log ((n : ℝ) + 1) + Real.log ((n ! : ℕ) : ℝ) := by      rw [Nat.factorial_succ]      push_cast      rw [Real.log_mul (by positivity) (by exact_mod_cast n.factorial_ne_zero)]    rw [← ofReal_add]    exact_mod_cast congrArg (fun t : ℝ => (t : ℂ)) hfac  have hlog : log (z + ((n + 1 : ℕ) : ℂ))      = (Real.log ((n : ℝ) + 1) : ℂ) + log (1 + z / ((n : ℂ) + 1)) := by    have hxx : ((((n : ℝ) + 1) : ℝ) : ℂ) * (1 + z / ((n : ℂ) + 1)) = z + ((n + 1 : ℕ) : ℂ) := by      push_cast      field_simp      ring    rw [← hxx, log_ofReal_mul hn1 hx]  unfold logGammaSeq  rw [Finset.sum_range_succ, hfacC, hlog]  push_cast  ring