feat: lemmas about ordered modules

src/Init/Grind/Module/Basic.lean

@@ -113,6 +113,12 @@ theorem sub_eq_iff {a b c : M} : a - b = c ↔ a = c + b := by
 theorem sub_eq_zero_iff {a b : M} : a - b = 0 ↔ a = b := by
   simp [sub_eq_iff, zero_add]
 
+theorem add_sub_cancel {a b : M} : a + b - b = a := by
+  rw [sub_eq_add_neg, add_assoc, add_neg_cancel, add_zero]
+
+theorem sub_add_cancel {a b : M} : a - b + b = a := by
+  rw [sub_eq_add_neg, add_assoc, neg_add_cancel, add_zero]
+
 theorem neg_hmul (n : Int) (a : M) : (-n) * a = - (n * a) := by
   apply (add_left_inj (n * a)).mp
   rw [← add_hmul, Int.add_left_neg, zero_hmul, neg_add_cancel]
@@ -121,6 +127,12 @@ theorem hmul_neg (n : Int) (a : M) : n * (-a) = - (n * a) := by
   apply (add_left_inj (n * a)).mp
   rw [← hmul_add, neg_add_cancel, neg_add_cancel, hmul_zero]
 
+theorem hmul_sub (k : Int) (a b : M) : k * (a - b) = k * a - k * b := by
+  rw [sub_eq_add_neg, hmul_add, hmul_neg, ← sub_eq_add_neg]
+
+theorem sub_hmul (k₁ k₂ : Int) (a : M) : (k₁ - k₂) * a = k₁ * a - k₂ * a := by
+  rw [Int.sub_eq_add_neg, add_hmul, neg_hmul, ← sub_eq_add_neg]
+
 end IntModule
 
 /--

src/Init/Grind/Ordered/Module.lean

@@ -103,12 +103,59 @@ theorem add_lt_right (a : M) {b c : M} (h : b < c) : a + b < a + c := by
   rw [add_comm a b, add_comm a c]
   exact add_lt_left h a
 
+theorem add_le_left_iff {a b : M} (c : M) : a ≤ b ↔ a + c ≤ b + c := by
+  constructor
+  · intro w
+    exact add_le_left w c
+  · intro w
+    have := add_le_left w (-c)
+    rwa [add_assoc, add_neg_cancel, add_zero, add_assoc, add_neg_cancel, add_zero] at this
+
+theorem add_le_right_iff {a b : M} (c : M) : a ≤ b ↔ c + a ≤ c + b := by
+  constructor
+  · intro w
+    exact add_le_right c w
+  · intro w
+    have := add_le_right (-c) w
+    rwa [← add_assoc, neg_add_cancel, zero_add, ← add_assoc, neg_add_cancel, zero_add] at this
+
+theorem add_lt_left_iff {a b : M} (c : M) : a < b ↔ a + c < b + c := by
+  constructor
+  · intro w
+    exact add_lt_left w c
+  · intro w
+    have := add_lt_left w (-c)
+    rwa [add_assoc, add_neg_cancel, add_zero, add_assoc, add_neg_cancel, add_zero] at this
+
+theorem add_lt_right_iff {a b : M} (c : M) : a < b ↔ c + a < c + b := by
+  constructor
+  · intro w
+    exact add_lt_right c w
+  · intro w
+    have := add_lt_right (-c) w
+    rwa [← add_assoc, neg_add_cancel, zero_add, ← add_assoc, neg_add_cancel, zero_add] at this
+
+theorem sub_nonneg_iff {a b : M} : 0 ≤ a - b ↔ b ≤ a := by
+  rw [add_le_left_iff b, zero_add, sub_add_cancel]
+
 theorem hmul_neg (k : Int) {a : M} (h : a < 0) : 0 < k ↔ k * a < 0 := by
   simpa [IntModule.hmul_neg, neg_pos_iff] using hmul_pos k (neg_pos_iff.mpr h)
 
 theorem hmul_nonpos {k : Int} {a : M} (hk : 0 ≤ k) (ha : a ≤ 0) : k * a ≤ 0 := by
   simpa [IntModule.hmul_neg, neg_nonneg_iff] using hmul_nonneg hk (neg_nonneg_iff.mpr ha)
 
+theorem hmul_le_hmul_of_le_of_le_of_nonneg_of_nonneg
+    {k₁ k₂ : Int} {x y : M} (hk : k₁ ≤ k₂) (h : x ≤ y) (w : 0 ≤ k₁) (w' : 0 ≤ x) :
+    k₁ * x ≤ k₂ * y := by
+  apply Preorder.le_trans
+  · have : 0 ≤ k₁ * (y - x) := hmul_nonneg w (sub_nonneg_iff.mpr h)
+    rwa [IntModule.hmul_sub, sub_nonneg_iff] at this
+  · have : 0 ≤ (k₂ - k₁) * y := hmul_nonneg (Int.sub_nonneg.mpr hk) (Preorder.le_trans w' h)
+    rwa [IntModule.sub_hmul, sub_nonneg_iff] at this
+
+theorem add_le_add {a b c d : M} (hab : a ≤ b) (hcd : c ≤ d) : a + c ≤ b + d :=
+  Preorder.le_trans (add_le_right a hcd) (add_le_left hab d)
+
 end IntModule.IsOrdered
 
 end Lean.Grind