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

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

State before:
a b c d : ℤ
⊢ |a - c| ≤ |a - b| + |b - c|
Tactic:
rewrite [show a - c = (a - b) + (b - c)
         by rw [←Int.add_sub_assoc, Int.sub_add_cancel]]
State after:
a b c d : ℤ
⊢ |a - b + (b - c)| ≤ |a - b| + |b - c|

State before:
a b c d : ℤ
⊢ |a - b + (b - c)| ≤ |a - b| + |b - c|
Tactic:
apply Int.natAbs_add_le
State after:
no goals

State before:
a b c d : ℤ
⊢ a - c = a - b + (b - c)
Tactic:
rw [←Int.add_sub_assoc, Int.sub_add_cancel]
State after:
no goals