no goals
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ val (-a) = val (-a) % n
rw [Nat.mod_eq_of_lt (-a).val_lt]
no goals
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ val (-a) + ?m.539514 a ≡ n - val a + ?m.539514 a [MOD n]
rw [Nat.ModEq, ← val_add, add_left_neg, tsub_add_cancel_of_le a.val_le, Nat.mod_self,
  val_zero]