Theorem: Perron.integralPosAux (PrimeNumberTheoremAnd/PerronFormula.lean)

State before:
x σ σ' σ'' T : ℝ
⊢ 0 < ∫ (t : ℝ), 1 / (√(1 + t ^ 2) * √(2 + t ^ 2))
Tactic:
apply integralPosAux' <;> norm_num
State after:
no goals