English
For any n > 0 and a ∈ ZMod n, the value of the negation is the remainder of n − a.val modulo n, i.e., (-a).val = (n − a.val) mod n.
Русский
Для любого n > 0 и a ∈ ZMod n значение отрицания равно остатку от n − a.val по модулю n: (-a).val = (n − a.val) mod n.
LaTeX
$$$(-a).val = (n - a.val) \bmod n$$$
Lean4
theorem neg_val' {n : ℕ} [NeZero n] (a : ZMod n) : (-a).val = (n - a.val) % n :=
calc
(-a).val = val (-a) % n := by rw [Nat.mod_eq_of_lt (-a).val_lt]
_ = (n - val a) % n :=
Nat.ModEq.add_right_cancel' (val a)
(by rw [Nat.ModEq, ← val_add, neg_add_cancel, tsub_add_cancel_of_le a.val_le, Nat.mod_self, val_zero])
