n : ℕ
⊢ 0 < ↑(succ n)! / (Real.sqrt (2 * ↑(succ n)) * (↑(succ n) / exp 1) ^ succ n)
n : ℕ
⊢ 0 < stirlingSeq (succ n)
unfold stirlingSeq
no goals
n : ℕ
⊢ 0 < ↑(succ n)! / (Real.sqrt (2 * ↑(succ n)) * (↑(succ n) / exp 1) ^ succ n)
positivity