have c₂_pos : 0 < c₂ := by linarith
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
⊢ 0 < ∫ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
⊢ 0 < ∫ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))