a b : Int
⊢ natAbs (a - b) ≤ natAbs a + natAbs (-b)
a b : Int
⊢ natAbs (a - b) ≤ natAbs a + natAbs b
rw [← Int.natAbs_neg b]
no goals
a b : Int
⊢ natAbs (a - b) ≤ natAbs a + natAbs (-b)
apply natAbs_add_le