gcongr
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))
t : ℝ
⊢ 1 / (√(c₁ + t ^ 2) * √(c₂ + t ^ 2)) ≤ 1 / (c₁ + t ^ 2)
case h
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))
t : ℝ
⊢ c₁ + t ^ 2 ≤ √(c₁ + t ^ 2) * √(c₂ + t ^ 2)