class Lean.Grind.IntModule.IsOrdered (M : Type u) [Preorder M] [IntModule M] : Prop

• neg_le_iff (a b : M) : -a ≤ b ↔ -b ≤ a
• add_le_left {a b : M} : a ≤ b → ∀ (c : M), a + c ≤ b + c
• hmul_pos (k : Int) {a : M} : 0 < a → (0 < k ↔ 0 < k * a)
• hmul_nonneg {k : Int} {a : M} : 0 ≤ k → 0 ≤ a → 0 ≤ k * a

theorem Lean.Grind.IntModule.IsOrdered.le_neg_iff {M : Type u} [Preorder M] [IntModule M] [IsOrdered M] {a b : M} : a ≤ -b ↔ b ≤ -a

theorem Lean.Grind.IntModule.IsOrdered.neg_lt_iff {M : Type u} [Preorder M] [IntModule M] [IsOrdered M] {a b : M} : -a < b ↔ -b < a

theorem Lean.Grind.IntModule.IsOrdered.lt_neg_iff {M : Type u} [Preorder M] [IntModule M] [IsOrdered M] {a b : M} : a < -b ↔ b < -a

theorem Lean.Grind.IntModule.IsOrdered.neg_nonneg_iff {M : Type u} [Preorder M] [IntModule M] [IsOrdered M] {a : M} : 0 ≤ -a ↔ a ≤ 0

theorem Lean.Grind.IntModule.IsOrdered.neg_pos_iff {M : Type u} [Preorder M] [IntModule M] [IsOrdered M] {a : M} : 0 < -a ↔ a < 0

theorem Lean.Grind.IntModule.IsOrdered.add_lt_left {M : Type u} [Preorder M] [IntModule M] [IsOrdered M] {a b : M} (h : a < b) (c : M) : a + c < b + c

theorem Lean.Grind.IntModule.IsOrdered.add_le_right {M : Type u} [Preorder M] [IntModule M] [IsOrdered M] (a : M) {b c : M} (h : b ≤ c) : a + b ≤ a + c

theorem Lean.Grind.IntModule.IsOrdered.add_lt_right {M : Type u} [Preorder M] [IntModule M] [IsOrdered M] (a : M) {b c : M} (h : b < c) : a + b < a + c

theorem Lean.Grind.IntModule.IsOrdered.hmul_neg {M : Type u} [Preorder M] [IntModule M] [IsOrdered M] (k : Int) {a : M} (h : a < 0) : 0 < k ↔ k * a < 0

theorem Lean.Grind.IntModule.IsOrdered.hmul_nonpos {M : Type u} [Preorder M] [IntModule M] [IsOrdered M] {k : Int} {a : M} (hk : 0 ≤ k) (ha : a ≤ 0) : k * a ≤ 0