let C := ∫ (t : ℝ), 1 / ((1 + t ^ 2).sqrt * (2 + t ^ 2).sqrt)
x σ σ' σ'' T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
h_contourPull : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
⊢ ∃ C > 0, ∀ σ' > 1, ‖VerticalIntegral (f x) σ'‖ ≤ x ^ σ' * C
x σ σ' σ'' T : ℝ
xpos : 0 < x
x_lt_one : x < 1
σ_pos : 0 < σ
h_contourPull : ∀ (σ' σ'' : ℝ), 0 < σ' → 0 < σ'' → VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ''
C : ℝ := ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))
⊢ ∃ C > 0, ∀ σ' > 1, ‖VerticalIntegral (f x) σ'‖ ≤ x ^ σ' * C