English
There is a canonical embedding of integers into ZNum, sending nonnegative integers to Num and negatives to the corresponding negative-numeric representation.
Русский
Существует каноническое вложение целых чисел в ZNum: неотрицательные преобразуются в соответствующее число, отрицательные — в представление отрицательного значения.
LaTeX
$$$\\operatorname{ofInt'} : \\mathbb{Z} \\to \\operatorname{ZNum},\\; \\operatorname{ofInt'}(\\operatorname{Int.ofNat} n) = \\operatorname{Num.toZNum}(\\operatorname{Num.ofNat'}(n)),\\; \\operatorname{ofInt'}(\\operatorname{Int.negSucc} n) = \\operatorname{Num.toZNumNeg}(\\operatorname{Num.ofNat'}(n+1)).$$$
Lean4
/-- Converts an `Int` to a `ZNum`. -/
def ofInt' : ℤ → ZNum
| Int.ofNat n => Num.toZNum (Num.ofNat' n)
| Int.negSucc n => Num.toZNumNeg (Num.ofNat' (n + 1))
