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

State before:
a b c d : ℤ
⊢ diff a b = diff b a
Tactic:
unfold diff
State after:
a b c d : ℤ
⊢ |a - b| = |b - a|

State before:
a b c d : ℤ
⊢ |a - b| = |b - a|
Tactic:
rw [←Int.natAbs_neg, Int.neg_sub]
State after:
no goals