constructor
case h.mpr.inr.intro
x : ℝ
hm4le : -4 ≤ x
hm3ge : x ≤ -3
⊢ 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19
case h.mpr.inr.intro.left
x : ℝ
hm4le : -4 ≤ x
hm3ge : x ≤ -3
⊢ 12 ≤ x ^ 2 + 3

case h.mpr.inr.intro.right
x : ℝ
hm4le : -4 ≤ x
hm3ge : x ≤ -3
⊢ x ^ 2 + 3 ≤ 19