There are lots of missing bits here. For instance, you seem to assume that a = sign(a) * abs(a). Why?

And both sign and abs are not defined. So you say abs(a) >= 0 and sign(a) \in {-1, 1}. Why? For instance, what is sign(0)?

Are you assuming a construction of integers from the natural numbers such that for any n < 0, there is an integer abs(n) and n = -1 * abs(n)? If so, don't you need to include that (or at least reference it)?

Later you assume that all integers are even or odd. Why?

These are niggling details that don't matter when you have chalk in hand, but do matter when speaking to a system like lean4.