calc
  _ ≤ (c₂ + t ^ 2).sqrt * (c₂ + t ^ 2).sqrt := by gcongr
  _ ≤ c₂ + t ^ 2 := by rw [← Real.sqrt_mul, sqrt_mul_self] <;> positivity
case h
x σ σ' σ'' T c₁ c₂ : ℝ
c₁_pos : 0 < c₁
hle : c₁ ≤ c₂
c₂_pos : 0 < c₂
t : ℝ
⊢ √(c₁ + t ^ 2) * √(c₂ + t ^ 2) ≤ c₂ + t ^ 2
no goals