constructor
case h.left
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ 3 ≤ Real.sqrt (x - 3) ∧ Real.sqrt (x - 3) ≤ 5
case h.left.left
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ 3 ≤ Real.sqrt (x - 3)

case h.left.right
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ Real.sqrt (x - 3) ≤ 5