no goals
n : ℕ
⊢ Real.log (stirlingSeq (succ n)) =
    Real.log ↑(succ n)! - 1 / 2 * Real.log (2 * ↑(succ n)) - ↑(succ n) * Real.log (↑(succ n) / exp 1)
rw [stirlingSeq, log_div, log_mul, sqrt_eq_rpow, log_rpow, Real.log_pow, tsub_tsub] <;> positivity