feat: Small lemmas around |a - b| and Int.natAbs (a - b) (#10027)

Proves the following statements:
- if `0 ≤ a ≤ n` and `0 ≤ b ≤ n`, then `|a - b| ≤ n` (similarly with `|a - b| < n`)
- `0 < |a - b|` iff `a ≠ b`



Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Mathlib/Algebra/Order/Group/Abs.lean

@@ -456,6 +456,18 @@ theorem abs_abs_sub_abs_le_abs_sub (a b : α) : |(|a| - |b|)| ≤ |a - b| :=
     ⟨abs_sub_abs_le_abs_sub _ _, by rw [abs_sub_comm]; apply abs_sub_abs_le_abs_sub⟩
 #align abs_abs_sub_abs_le_abs_sub abs_abs_sub_abs_le_abs_sub
 
+/-- `|a - b| ≤ n` if `0 ≤ a ≤ n` and `0 ≤ b ≤ n`. -/
+theorem abs_sub_le_of_nonneg_of_le {a b n : α} (a_nonneg : 0 ≤ a) (a_le_n : a ≤ n)
+    (b_nonneg : 0 ≤ b) (b_le_n : b ≤ n) : |a - b| ≤ n := by
+  rw [abs_sub_le_iff, sub_le_iff_le_add, sub_le_iff_le_add]
+  exact ⟨le_add_of_le_of_nonneg a_le_n b_nonneg, le_add_of_le_of_nonneg b_le_n a_nonneg⟩
+
+/-- `|a - b| < n` if `0 ≤ a < n` and `0 ≤ b < n`. -/
+theorem abs_sub_lt_of_nonneg_of_lt {a b n : α} (a_nonneg : 0 ≤ a) (a_lt_n : a < n)
+    (b_nonneg : 0 ≤ b) (b_lt_n : b < n) : |a - b| < n := by
+  rw [abs_sub_lt_iff, sub_lt_iff_lt_add, sub_lt_iff_lt_add]
+  exact ⟨lt_add_of_lt_of_nonneg a_lt_n b_nonneg, lt_add_of_lt_of_nonneg b_lt_n a_nonneg⟩
+
 theorem abs_eq (hb : 0 ≤ b) : |a| = b ↔ a = b ∨ a = -b := by
   refine' ⟨eq_or_eq_neg_of_abs_eq, _⟩
   rintro (rfl | rfl) <;> simp only [abs_neg, abs_of_nonneg hb]
@@ -510,6 +522,12 @@ theorem eq_of_abs_sub_nonpos (h : |a - b| ≤ 0) : a = b :=
   eq_of_abs_sub_eq_zero (le_antisymm h (abs_nonneg (a - b)))
 #align eq_of_abs_sub_nonpos eq_of_abs_sub_nonpos
 
+theorem abs_sub_nonpos : |a - b| ≤ 0 ↔ a = b :=
+  ⟨eq_of_abs_sub_nonpos, by rintro rfl; rw [sub_self, abs_zero]⟩
+
+theorem abs_sub_pos : 0 < |a - b| ↔ a ≠ b :=
+  not_le.symm.trans abs_sub_nonpos.not
+
 @[simp]
 theorem abs_eq_self : |a| = a ↔ 0 ≤ a := by
   rw [abs_eq_max_neg, max_eq_left_iff, neg_le_self_iff]

Mathlib/Data/Int/Lemmas.lean

@@ -77,6 +77,22 @@ theorem natAbs_inj_of_nonpos_of_nonneg {a b : ℤ} (ha : a ≤ 0) (hb : 0 ≤ b)
   simpa only [Int.natAbs_neg] using natAbs_inj_of_nonneg_of_nonneg (neg_nonneg_of_nonpos ha) hb
 #align int.nat_abs_inj_of_nonpos_of_nonneg Int.natAbs_inj_of_nonpos_of_nonneg
 
+/-- A specialization of `abs_sub_le_of_nonneg_of_le` for working with the signed subtraction
+  of natural numbers. -/
+theorem natAbs_coe_sub_coe_le_of_le {a b n : ℕ} (a_le_n : a ≤ n) (b_le_n : b ≤ n) :
+    natAbs (a - b : ℤ) ≤ n := by
+  rw [← Nat.cast_le (α := ℤ), coe_natAbs]
+  exact abs_sub_le_of_nonneg_of_le (ofNat_nonneg a) (ofNat_le.mpr a_le_n)
+    (ofNat_nonneg b) (ofNat_le.mpr b_le_n)
+
+/-- A specialization of `abs_sub_lt_of_nonneg_of_lt` for working with the signed subtraction
+  of natural numbers. -/
+theorem natAbs_coe_sub_coe_lt_of_lt {a b n : ℕ} (a_lt_n : a < n) (b_lt_n : b < n) :
+    natAbs (a - b : ℤ) < n := by
+  rw [← Nat.cast_lt (α := ℤ), coe_natAbs]
+  exact abs_sub_lt_of_nonneg_of_lt (ofNat_nonneg a) (ofNat_lt.mpr a_lt_n)
+    (ofNat_nonneg b) (ofNat_lt.mpr b_lt_n)
+
 section Intervals
 
 open Set

Mathlib/Data/Int/Order/Basic.lean

@@ -121,6 +121,11 @@ lemma cast_mul_eq_zsmul_cast {α : Type*} [AddCommGroupWithOne α] :
     simp only [sub_mul, one_mul, cast_sub, ih, sub_zsmul, one_zsmul, ← sub_eq_add_neg, forall_const]
 #align int.cast_mul_eq_zsmul_cast Int.cast_mul_eq_zsmul_cast
 
+theorem natAbs_sub_pos_iff {i j : ℤ} : 0 < natAbs (i - j) ↔ i ≠ j := by
+  rw [natAbs_pos, ne_eq, sub_eq_zero]
+
+theorem natAbs_sub_ne_zero_iff {i j : ℤ} : natAbs (i - j) ≠ 0 ↔ i ≠ j :=
+  Nat.ne_zero_iff_zero_lt.trans natAbs_sub_pos_iff
 
 /-! ### succ and pred -/