lift x to ℕ using (by linarith)
f : ℤ → ℂ
m n : ℕ
x : ℤ
hx : ↑m < x ∧ x ≤ ↑n
⊢ ∃ x_1, (m < x_1 ∧ x_1 ≤ n) ∧ ↑x_1 = x
case intro
f : ℤ → ℂ
m n x : ℕ
hx : ↑m < ↑x ∧ ↑x ≤ ↑n
⊢ ∃ x_1, (m < x_1 ∧ x_1 ≤ n) ∧ ↑x_1 = ↑x