You're right that a lot that is "usually defined" in math has to be explicitly defined in theorem prover/proof assistant

* abs(x) is usually defined as "x if x >=0 and -x if x < 0"

* sign(x) is usually defined as "1 if x >=0 and -1 if x < 0"

* with these definitions, it follows that for any x, x = sign(x) * abs(x) (by definition applied for each cases >=0 and <0, assuming that all integer are either >=0 or <0)

Showing that any integer is either even or odd seem less obvious