English
For [NeZero n], (a.valMinAbs.natAbs : ZMod n) equals if a.val ≤ n/2 then a else -a.
Русский
Для [NeZero n] (a.valMinAbs.natAbs : ZMod n) равно, если a.val ≤ n/2, то a, иначе -a.
LaTeX
$$$[\\mathrm{NeZero}\\ n]\\ (a : \\mathbb{Z}/n\\mathbb{Z}).valMinAbs.natAbs = \\text{if } a.val \\le \\frac{n}{2} \\text{ then } a \\text{ else } -a$$$
Lean4
theorem natCast_natAbs_valMinAbs [NeZero n] (a : ZMod n) :
(a.valMinAbs.natAbs : ZMod n) = if a.val ≤ (n : ℕ) / 2 then a else -a :=
by
have : (a.val : ℤ) - n ≤ 0 := by
rw [sub_nonpos, Int.ofNat_le]
exact a.val_le
rw [valMinAbs_def_pos]
split_ifs
· rw [Int.natAbs_natCast, natCast_zmod_val]
·
rw [← Int.cast_natCast, Int.ofNat_natAbs_of_nonpos this, Int.cast_neg, Int.cast_sub, Int.cast_natCast,
Int.cast_natCast, natCast_self, sub_zero, natCast_zmod_val]
