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

case h.right
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ Real.sqrt (x - 3) ^ 2 + 3 = x