constructor
case h.mpr.inl.intro
x : ℝ
h3le : 3 ≤ x
h4ge : x ≤ 4
⊢ 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19
case h.mpr.inl.intro.left
x : ℝ
h3le : 3 ≤ x
h4ge : x ≤ 4
⊢ 12 ≤ x ^ 2 + 3

case h.mpr.inl.intro.right
x : ℝ
h3le : 3 ≤ x
h4ge : x ≤ 4
⊢ x ^ 2 + 3 ≤ 19