theorem
Lean.Grind.OrderedAdd.add_le_right_iff
{M : Type u}
[Preorder M]
[AddCommMonoid M]
[OrderedAdd M]
{a b : M}
(c : M)
:
theorem
Lean.Grind.OrderedAdd.add_le_left
{M : Type u}
[Preorder M]
[AddCommMonoid M]
[OrderedAdd M]
{a b : M}
(h : a ≤ b)
(c : M)
:
theorem
Lean.Grind.OrderedAdd.add_le_right
{M : Type u}
[Preorder M]
[AddCommMonoid M]
[OrderedAdd M]
{a b : M}
(c : M)
(h : a ≤ b)
:
theorem
Lean.Grind.OrderedAdd.add_lt_left
{M : Type u}
[Preorder M]
[AddCommMonoid M]
[OrderedAdd M]
{a b : M}
(h : a < b)
(c : M)
:
theorem
Lean.Grind.OrderedAdd.add_lt_right
{M : Type u}
[Preorder M]
[AddCommMonoid M]
[OrderedAdd M]
{a b : M}
(c : M)
(h : a < b)
:
theorem
Lean.Grind.OrderedAdd.add_lt_left_iff
{M : Type u}
[Preorder M]
[AddCommMonoid M]
[OrderedAdd M]
{a b : M}
(c : M)
:
theorem
Lean.Grind.OrderedAdd.add_lt_right_iff
{M : Type u}
[Preorder M]
[AddCommMonoid M]
[OrderedAdd M]
{a b : M}
(c : M)
:
theorem
Lean.Grind.OrderedAdd.add_le_add
{M : Type u}
[Preorder M]
[AddCommMonoid M]
[OrderedAdd M]
{a b c d : M}
(hab : a ≤ b)
(hcd : c ≤ d)
:
theorem
Lean.Grind.OrderedAdd.nsmul_nonneg
{M : Type u}
[Preorder M]
[NatModule M]
[OrderedAdd M]
{k : Nat}
{a : M}
(h : 0 ≤ a)
:
theorem
Lean.Grind.OrderedAdd.neg_le_iff
{M : Type u}
[Preorder M]
[AddCommGroup M]
[OrderedAdd M]
{a b : M}
:
theorem
Lean.Grind.OrderedAdd.le_neg_iff
{M : Type u}
[Preorder M]
[AddCommGroup M]
[OrderedAdd M]
{a b : M}
:
theorem
Lean.Grind.OrderedAdd.neg_lt_iff
{M : Type u}
[Preorder M]
[AddCommGroup M]
[OrderedAdd M]
{a b : M}
:
theorem
Lean.Grind.OrderedAdd.lt_neg_iff
{M : Type u}
[Preorder M]
[AddCommGroup M]
[OrderedAdd M]
{a b : M}
:
theorem
Lean.Grind.OrderedAdd.neg_nonneg_iff
{M : Type u}
[Preorder M]
[AddCommGroup M]
[OrderedAdd M]
{a : M}
:
theorem
Lean.Grind.OrderedAdd.neg_pos_iff
{M : Type u}
[Preorder M]
[AddCommGroup M]
[OrderedAdd M]
{a : M}
:
theorem
Lean.Grind.OrderedAdd.sub_nonneg_iff
{M : Type u}
[Preorder M]
[AddCommGroup M]
[OrderedAdd M]
{a b : M}
:
theorem
Lean.Grind.OrderedAdd.sub_pos_iff
{M : Type u}
[Preorder M]
[AddCommGroup M]
[OrderedAdd M]
{a b : M}
: