Theorem: BrownCs22.Int.ModEq.neg (BrownCs22/Library/ModEq/Lemmas.lean)

State before:
n a b : ℤ
h1 : a ≡ b [ZMOD n]
⊢ -a ≡ -b [ZMOD n]
Tactic:
obtain ⟨x, hx⟩ := h1
State after:
case intro
n a b x : ℤ
hx : a - b = n * x
⊢ -a ≡ -b [ZMOD n]

State before:
case intro
n a b x : ℤ
hx : a - b = n * x
⊢ -a ≡ -b [ZMOD n]
Tactic:
exact ⟨-x, by linear_combination -hx⟩
State after:
no goals

State before:
n a b x : ℤ
hx : a - b = n * x
⊢ -a - -b = n * -x
Tactic:
linear_combination -hx
State after:
no goals