Theorem: LoVe.Int.neg_eq (LoVe/Labs/Lab8Solution.lean)

State before:
p n : ℕ
⊢ neg (Quotient.mk Setoid (p, n)) = Quotient.mk Setoid (n, p)
Tactic:
rfl
State after:
no goals