have hupper (t : ℝ) : 1 / ((c₁ + t ^ 2).sqrt * (c₂ + t ^ 2).sqrt) ≤ 1 / (c₁ + t ^ 2)  := by
    gcongr
    calc
      _ ≥ (c₁ + t ^ 2).sqrt * (c₁ + t ^ 2).sqrt := by gcongr
      _ ≥ c₁ + t ^ 2 := by rw [← Real.sqrt_mul, sqrt_mul_self] <;> positivity
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
hlower : ∀ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
⊢ 0 < ∫ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
hlower : ∀ (t : ℝ), 1 / (c₂ + t ^ 2) ≤ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))
hupper : ∀ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2)) ≤ 1 / (c₁ + t ^ 2)
⊢ 0 < ∫ (t : ℝ), 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2))