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

State before:
m : Nat
⊢ m + 1 ⊖ 0 = ofNat (m + 1)
Tactic:
rw [Int.mk, Int.subNatNat, Nat.zero_sub, Nat.sub_zero]
State after:
no goals