Theorem: Int.succ_mk_succ (Extra/Int/Basic.lean)

State before:
m n : Nat
⊢ m + 1 ⊖ n + 1 = m ⊖ n
Tactic:
rw [Int.mk, Int.subNatNat, Int.subNatNat, Nat.succ_sub_succ, Nat.succ_sub_succ]
State after:
no goals