chore: exchange Nat.sub_lt_iff_lt_add and Nat.sub_lt_iff_lt_add' (#24080)

This PR swaps `Nat.sub_lt_iff_lt_add` and `Nat.sub_lt_iff_lt_add'` to align them with the top-level `sub_lt_iff_lt_add` and `sub_lt_iff_lt_add'` lemmas.

leanprover/lean4#7971 will upstream these lemmas with this swapped meaning.



Co-authored-by: Markus Himmel <markus@lean-fro.org>

Author: TwoFX

Archive/Imo/Imo2024Q3.lean

@@ -139,7 +139,7 @@ lemma apply_nth_add_one_eq_of_lt {m n : ℕ} (hn : N < Nat.nth (a · = m) n) :
 
 lemma lt_toFinset_card {j : ℕ} (h : M a N ≤ a (j + 1)) (hf : {i | a i = a j}.Finite) :
     M a N - 1 < #hf.toFinset := by
-  rw [Nat.sub_lt_iff_lt_add (M_pos _ _), Nat.lt_one_add_iff]
+  rw [Nat.sub_lt_iff_lt_add' (M_pos _ _), Nat.lt_one_add_iff]
   exact (hc.apply_eq_card (N_lt_of_M_le_apply h) ▸ h).trans (Finset.card_le_card (by simp))
 
 lemma nth_ne_zero_of_M_le_of_lt {i k : ℕ} (hi : M a N ≤ a i) (hk : k < a (i + 1)) :
@@ -636,7 +636,7 @@ lemma apply_add_one_eq_card_small_le_card_eq {i : ℕ} (hi : N' a N < i) (hib :
       rw [← Nat.count_eq_card_filter_range] at htr
       constructor
       · rwa [add_lt_add_iff_right, ← Nat.lt_nth_iff_count_lt hts,
-          Nat.sub_lt_iff_lt_add (hc.one_le_apply _), Nat.lt_one_add_iff]
+          Nat.sub_lt_iff_lt_add' (hc.one_le_apply _), Nat.lt_one_add_iff]
       · rw [hc.apply_nth_add_one_eq_of_infinite hts]
         · exact Nat.sub_add_cancel (hc.one_le_apply _)
         · refine (Nat.le_nth fun hf ↦ absurd hf hts).trans ((Nat.nth_le_nth hts).2 ?_)

Mathlib/Data/List/Rotate.lean

@@ -199,11 +199,11 @@ theorem getElem?_rotate {l : List α} {n m : ℕ} (hml : m < l.length) :
       rw [length_drop] at hm
       have hm' := Nat.sub_le_iff_le_add'.1 hm
       have : n % length l + m - length l < length l := by
-        rw [Nat.sub_lt_iff_lt_add' hm']
+        rw [Nat.sub_lt_iff_lt_add hm']
         exact Nat.add_lt_add hlt hml
       conv_rhs => rw [Nat.add_comm m, ← mod_add_mod, mod_eq_sub_mod hm', mod_eq_of_lt this]
       omega
-    · rwa [Nat.sub_lt_iff_lt_add hm, length_drop, Nat.sub_add_cancel hlt.le]
+    · rwa [Nat.sub_lt_iff_lt_add' hm, length_drop, Nat.sub_add_cancel hlt.le]
 
 theorem getElem_rotate (l : List α) (n : ℕ) (k : Nat) (h : k < (l.rotate n).length) :
     (l.rotate n)[k] =

Mathlib/Data/Nat/Init.lean

@@ -244,8 +244,8 @@ protected lemma eq_sub_of_add_eq' (h : b + c = a) : c = a - b := by omega
 
 protected lemma lt_sub_iff_add_lt : a < c - b ↔ a + b < c := ⟨add_lt_of_lt_sub, lt_sub_of_add_lt⟩
 protected lemma lt_sub_iff_add_lt' : a < c - b ↔ b + a < c := by omega
-protected lemma sub_lt_iff_lt_add (hba : b ≤ a) : a - b < c ↔ a < b + c := by omega
-protected lemma sub_lt_iff_lt_add' (hba : b ≤ a) : a - b < c ↔ a < c + b := by omega
+protected lemma sub_lt_iff_lt_add (hba : b ≤ a) : a - b < c ↔ a < c + b := by omega
+protected lemma sub_lt_iff_lt_add' (hba : b ≤ a) : a - b < c ↔ a < b + c := by omega
 
 protected lemma sub_sub_sub_cancel_right (h : c ≤ b) : a - c - (b - c) = a - b := by omega
 protected lemma add_sub_sub_cancel (h : c ≤ a) : a + b - (a - c) = b + c := by omega
@@ -1033,7 +1033,7 @@ lemma add_mod_eq_ite :
     rw [Nat.add_mod]
     by_cases h : k + 1 ≤ m % (k + 1) + n % (k + 1)
     · rw [if_pos h, Nat.mod_eq_sub_mod h, Nat.mod_eq_of_lt]
-      exact (Nat.sub_lt_iff_lt_add h).mpr (Nat.add_lt_add (m.mod_lt (zero_lt_succ _))
+      exact (Nat.sub_lt_iff_lt_add' h).mpr (Nat.add_lt_add (m.mod_lt (zero_lt_succ _))
         (n.mod_lt (zero_lt_succ _)))
     · rw [if_neg h]
       exact Nat.mod_eq_of_lt (Nat.lt_of_not_ge h)

Mathlib/Order/WellFoundedSet.lean

@@ -776,7 +776,7 @@ theorem partiallyWellOrderedOn_sublistForall₂ (r : α → α → Prop) [IsPreo
     split_ifs at hmn with hm
     · apply hf1.2 m (g n') (lt_of_lt_of_le hm (g.monotone n'.zero_le))
       exact _root_.trans hmn (List.tail_sublistForall₂_self _)
-    · rw [← Nat.sub_lt_iff_lt_add (le_of_not_lt hm)] at mn
+    · rw [← Nat.sub_lt_iff_lt_add' (le_of_not_lt hm)] at mn
       apply hf1.2 _ _ (g.lt_iff_lt.2 mn)
       rw [← List.cons_head!_tail (hnil (g (m - g 0))), ← List.cons_head!_tail (hnil (g n'))]
       exact List.SublistForall₂.cons (hg _ _ (le_of_lt mn)) hmn