Theorem: Int.add_neg_self_right (Extra/Int/Lemmas.lean)

State before:
i : Int
⊢ i + -i = 0
Tactic:
cases i using Int.casesMkOn with
| mk mi ni => rw [neg_mk, mk_add_mk, Nat.add_comm mi ni, mk_self]
State after:
no goals

State before:
case mk
mi ni : Nat
⊢ (mi ⊖ ni) + -(mi ⊖ ni) = 0
Tactic:
rw [neg_mk, mk_add_mk, Nat.add_comm mi ni, mk_self]
State after:
no goals