Definition. int_eq
ℤ = {z | z ∈ ℝ ∧ ∃a. ∃b. a ∈ ℕ ∧ b ∈ ℕ ∧ z = a - b}