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

State before:
a b c d : ℤ
⊢ ↑(|a|) - ↑(|b|) ≤ ↑(|a - b|)
Tactic:
repeat rw [Int.coe_natAbs]
State after:
a b c d : ℤ
⊢ abs a - abs b ≤ abs (a - b)

State before:
a b c d : ℤ
⊢ abs a - abs b ≤ abs (a - b)
Tactic:
exact abs_sub_abs_le_abs_sub a b
State after:
no goals

State before:
a b c d : ℤ
⊢ abs a - abs b ≤ ↑(|a - b|)
Tactic:
rw [Int.coe_natAbs]
State after:
a b c d : ℤ
⊢ abs a - abs b ≤ abs (a - b)