constructor
case h
x : ℝ
⊢ 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19 ↔ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
case h.mp
x : ℝ
⊢ 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19 → 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3

case h.mpr
x : ℝ
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3 → 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19