feat: Nat.add_div_of_dvd_add_add_one (#7432)

This PR adds a consequence of `Nat.add_div` using a divisibility
hypothesis.

src/Init/Data/Nat/Div/Lemmas.lean

@@ -14,6 +14,31 @@ import Init.Data.Nat.Simproc
 
 namespace Nat
 
+theorem mod_add_mod_lt (a b : Nat) {c : Nat} (h : 0 < c) : a % c + b % c < 2 * c - 1 := by
+  have := mod_lt a h
+  have := mod_lt b h
+  omega
+
+theorem mod_add_mod_eq {a b c : Nat} : a % c + b % c = (a + b) % c + if a % c + b % c < c then 0 else c := by
+  if h : 0 < c then
+    rw [add_mod]
+    split <;> rename_i h'
+    · simp [mod_eq_of_lt h']
+    · have : (a % c + b % c) % c = a % c + b % c - c := by
+        rw [mod_eq_iff]
+        right
+        have := mod_lt a h
+        have := mod_lt b h
+        exact ⟨by omega, ⟨1, by simp; omega⟩⟩
+      omega
+  else
+    replace h : c = 0 := by omega
+    simp [h]
+
+theorem add_mod_eq_sub : (a + b) % c = a % c + b % c - if a % c + b % c < c then 0 else c := by
+  conv => rhs; congr; rw [mod_add_mod_eq]
+  omega
+
 theorem lt_div_iff_mul_lt (h : 0 < k) : x < y / k ↔ x * k < y - (k - 1) := by
   have t := le_div_iff_mul_le h (x := x + 1) (y := y)
   rw [succ_le, add_one_mul] at t
@@ -128,4 +153,19 @@ protected theorem add_div {a b c : Nat} (h : 0 < c) :
     have := mod_lt b h
     split <;> · simp; omega
 
+/-- If `(a + b) % c = c - 1`, then `a % c + b % c < c`, because `a % c + b % c` can not reach `2*c - 1`. -/
+theorem mod_add_mod_lt_of_add_mod_eq_sub_one (w : 0 < c) (h : (a + b) % c = c - 1) : a % c + b % c < c := by
+  have := mod_add_mod_lt a b w
+  rw [mod_add_mod_eq, h] at this
+  split at this
+  · assumption
+  · omega
+
+theorem add_div_of_dvd_add_add_one (h : c ∣ a + b + 1) : (a + b) / c = a / c + b / c := by
+  have w : c ≠ 0 := by rintro rfl; simp at h
+  replace w : 0 < c := by omega
+  rw [Nat.add_div w, if_neg, Nat.add_zero]
+  have := mod_add_mod_lt_of_add_mod_eq_sub_one w ((mod_eq_sub_iff Nat.zero_lt_one w).mpr h)
+  omega
+
 end Nat

src/Init/Data/Nat/Lemmas.lean

@@ -934,6 +934,25 @@ theorem mod_eq_iff {a b c : Nat} :
      · simp_all
      · rw [mul_add_mod, mod_eq_of_lt w]⟩
 
+theorem mod_eq_sub_iff {a b c : Nat} (h₁ : 0 < c) (h : c ≤ b) : a % b = b - c ↔ b ∣ a + c := by
+  rw [Nat.mod_eq_iff]
+  refine ⟨?_, ?_⟩
+  · rintro (⟨rfl, rfl⟩|⟨hlt, ⟨k, hk⟩⟩)
+    · simp; omega
+    · refine ⟨k + 1, ?_⟩
+      rw [← Nat.add_sub_assoc h] at hk
+      rw [Nat.mul_succ, eq_comm]
+      apply Nat.eq_add_of_sub_eq (by omega) hk.symm
+  · rintro ⟨k, hk⟩
+    obtain (rfl|hb) := Nat.eq_zero_or_pos b
+    · obtain rfl : c = 0 := by omega
+      refine Or.inl ⟨rfl, by simpa using hk⟩
+    · have : k ≠ 0 := by rintro rfl; omega
+      refine Or.inr ⟨by omega, ⟨k - 1, ?_⟩⟩
+      rw [← Nat.add_sub_assoc h, eq_comm]
+      apply Nat.sub_eq_of_eq_add
+      rw [mul_sub_one, Nat.sub_add_cancel (Nat.le_mul_of_pos_right _ (by omega)), hk]
+
 theorem succ_mod_succ_eq_zero_iff {a b : Nat} :
     (a + 1) % (b + 1) = 0 ↔ a % (b + 1) = b := by
   symm