Lemmas on Int.natAbs

theorem Int.sub_le_add_natAbs {a b : ℤ} : a.natAbs - b.natAbs ≤ (a + b).natAbs

theorem Int.natAbs_add_of_mul_nonneg {a b : ℤ} (h : 0 ≤ a * b) : (a + b).natAbs = a.natAbs + b.natAbs