case intro
d : ℝ
h : ∀ (n : ℕ), Real.log (stirlingSeq 1) - Real.log (stirlingSeq (succ n)) ≤ d
⊢ ∃ c, ∀ (n : ℕ), c ≤ Real.log (stirlingSeq (succ n))
⊢ ∃ c, ∀ (n : ℕ), c ≤ Real.log (stirlingSeq (succ n))
obtain ⟨d, h⟩ := log_stirlingSeq_bounded_aux
no goals
case intro
d : ℝ
h : ∀ (n : ℕ), Real.log (stirlingSeq 1) - Real.log (stirlingSeq (succ n)) ≤ d
⊢ ∃ c, ∀ (n : ℕ), c ≤ Real.log (stirlingSeq (succ n))
exact ⟨log (stirlingSeq 1) - d, fun n => sub_le_comm.mp (h n)⟩