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

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