Theorem: Int.diff_self_eq_zero (Util/Arithmetic.lean)

State before:
a b c d : ℤ
⊢ diff a a = 0
Tactic:
unfold diff natAbs
State after:
a b c d : ℤ
⊢ (match a - a with
    | ofNat m => m
    | -[m+1] => Nat.succ m) =
    0

State before:
a b c d : ℤ
⊢ (match a - a with
    | ofNat m => m
    | -[m+1] => Nat.succ m) =
    0
Tactic:
rw [Int.sub_self a]
State after:
no goals