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

State before:
m₁ n₁ m₂ n₂ : Nat
⊢ (m₁ ⊖ n₁) + -(m₂ ⊖ n₂) = m₁ + n₂ ⊖ n₁ + m₂
Tactic:
rw [neg_mk, mk_add_mk]
State after:
no goals