[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedSemiring k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
hc : 0 < c
⊢ c • a < 0 ↔ a < 0
[PROOFSTEP]
rw [← neg_neg a, smul_neg, neg_neg_iff_pos, neg_neg_iff_pos]
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedSemiring k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
hc : 0 < c
⊢ 0 < c • -a ↔ 0 < -a
[PROOFSTEP]
exact smul_pos_iff_of_pos hc
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
h : a < b
hc : c < 0
⊢ c • b < c • a
[PROOFSTEP]
rw [← neg_neg c, neg_smul, neg_smul (-c), neg_lt_neg_iff]
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
h : a < b
hc : c < 0
⊢ -c • a < -c • b
[PROOFSTEP]
exact smul_lt_smul_of_pos h (neg_pos_of_neg hc)
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
h : a ≤ b
hc : c ≤ 0
⊢ c • b ≤ c • a
[PROOFSTEP]
rw [← neg_neg c, neg_smul, neg_smul (-c), neg_le_neg_iff]
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
h : a ≤ b
hc : c ≤ 0
⊢ -c • a ≤ -c • b
[PROOFSTEP]
exact smul_le_smul_of_nonneg h (neg_nonneg_of_nonpos hc)
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
hab : c • a = c • b
hc : c < 0
h : a ≤ b
⊢ a = b
[PROOFSTEP]
rw [← neg_neg c, neg_smul, neg_smul (-c), neg_inj] at hab 
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
hab : -c • a = -c • b
hc : c < 0
h : a ≤ b
⊢ a = b
[PROOFSTEP]
exact eq_of_smul_eq_smul_of_pos_of_le hab (neg_pos_of_neg hc) h
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
h : c • a < c • b
hc : c ≤ 0
⊢ b < a
[PROOFSTEP]
rw [← neg_neg c, neg_smul, neg_smul (-c), neg_lt_neg_iff] at h 
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
h : -c • b < -c • a
hc : c ≤ 0
⊢ b < a
[PROOFSTEP]
exact lt_of_smul_lt_smul_of_nonneg h (neg_nonneg_of_nonpos hc)
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
hc : c < 0
⊢ c • a < c • b ↔ b < a
[PROOFSTEP]
rw [← neg_neg c, neg_smul, neg_smul (-c), neg_lt_neg_iff]
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
hc : c < 0
⊢ -c • b < -c • a ↔ b < a
[PROOFSTEP]
exact smul_lt_smul_iff_of_pos (neg_pos_of_neg hc)
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
hc : c < 0
⊢ c • a < 0 ↔ 0 < a
[PROOFSTEP]
rw [← neg_neg c, neg_smul, neg_neg_iff_pos]
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
hc : c < 0
⊢ 0 < -c • a ↔ 0 < a
[PROOFSTEP]
exact smul_pos_iff_of_pos (neg_pos_of_neg hc)
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
hc : c < 0
⊢ 0 < c • a ↔ a < 0
[PROOFSTEP]
rw [← neg_neg c, neg_smul, neg_pos]
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
hc : c < 0
⊢ -c • a < 0 ↔ a < 0
[PROOFSTEP]
exact smul_neg_iff_of_pos (neg_pos_of_neg hc)
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : OrderedRing k
inst✝³ : OrderedAddCommGroup M
inst✝² : Module k M
inst✝¹ : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : k
c d : M
hab : a ≤ b
hcd : c ≤ d
⊢ a • d + b • c ≤ a • c + b • d
[PROOFSTEP]
obtain ⟨b, rfl⟩ := exists_add_of_le hab
[GOAL]
case intro
k : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : OrderedRing k
inst✝³ : OrderedAddCommGroup M
inst✝² : Module k M
inst✝¹ : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a : k
c d : M
hcd : c ≤ d
b : k
hab : a ≤ a + b
⊢ a • d + (a + b) • c ≤ a • c + (a + b) • d
[PROOFSTEP]
obtain ⟨d, rfl⟩ := exists_add_of_le hcd
[GOAL]
case intro.intro
k : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : OrderedRing k
inst✝³ : OrderedAddCommGroup M
inst✝² : Module k M
inst✝¹ : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a : k
c : M
b : k
hab : a ≤ a + b
d : M
hcd : c ≤ c + d
⊢ a • (c + d) + (a + b) • c ≤ a • c + (a + b) • (c + d)
[PROOFSTEP]
rw [smul_add, add_right_comm, smul_add, ← add_assoc, add_smul _ _ d]
[GOAL]
case intro.intro
k : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : OrderedRing k
inst✝³ : OrderedAddCommGroup M
inst✝² : Module k M
inst✝¹ : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a : k
c : M
b : k
hab : a ≤ a + b
d : M
hcd : c ≤ c + d
⊢ a • c + (a + b) • c + a • d ≤ a • c + (a + b) • c + (a • d + b • d)
[PROOFSTEP]
rw [le_add_iff_nonneg_right] at hab hcd 
[GOAL]
case intro.intro
k : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : OrderedRing k
inst✝³ : OrderedAddCommGroup M
inst✝² : Module k M
inst✝¹ : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a : k
c : M
b : k
hab : 0 ≤ b
d : M
hcd : 0 ≤ d
⊢ a • c + (a + b) • c + a • d ≤ a • c + (a + b) • c + (a • d + b • d)
[PROOFSTEP]
exact add_le_add_left (le_add_of_nonneg_right <| smul_nonneg hab hcd) _
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : OrderedRing k
inst✝³ : OrderedAddCommGroup M
inst✝² : Module k M
inst✝¹ : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : k
c d : M
hba : b ≤ a
hdc : d ≤ c
⊢ a • d + b • c ≤ a • c + b • d
[PROOFSTEP]
rw [add_comm (a • d), add_comm (a • c)]
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : OrderedRing k
inst✝³ : OrderedAddCommGroup M
inst✝² : Module k M
inst✝¹ : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : k
c d : M
hba : b ≤ a
hdc : d ≤ c
⊢ b • c + a • d ≤ b • d + a • c
[PROOFSTEP]
exact smul_add_smul_le_smul_add_smul hba hdc
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : OrderedRing k
inst✝⁴ : OrderedAddCommGroup M
inst✝³ : Module k M
inst✝² : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝¹ : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a b : k
c d : M
hab : a < b
hcd : c < d
⊢ a • d + b • c < a • c + b • d
[PROOFSTEP]
obtain ⟨b, rfl⟩ := exists_add_of_le hab.le
[GOAL]
case intro
k : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : OrderedRing k
inst✝⁴ : OrderedAddCommGroup M
inst✝³ : Module k M
inst✝² : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝¹ : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a : k
c d : M
hcd : c < d
b : k
hab : a < a + b
⊢ a • d + (a + b) • c < a • c + (a + b) • d
[PROOFSTEP]
obtain ⟨d, rfl⟩ := exists_add_of_le hcd.le
[GOAL]
case intro.intro
k : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : OrderedRing k
inst✝⁴ : OrderedAddCommGroup M
inst✝³ : Module k M
inst✝² : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝¹ : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a : k
c : M
b : k
hab : a < a + b
d : M
hcd : c < c + d
⊢ a • (c + d) + (a + b) • c < a • c + (a + b) • (c + d)
[PROOFSTEP]
rw [smul_add, add_right_comm, smul_add, ← add_assoc, add_smul _ _ d]
[GOAL]
case intro.intro
k : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : OrderedRing k
inst✝⁴ : OrderedAddCommGroup M
inst✝³ : Module k M
inst✝² : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝¹ : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a : k
c : M
b : k
hab : a < a + b
d : M
hcd : c < c + d
⊢ a • c + (a + b) • c + a • d < a • c + (a + b) • c + (a • d + b • d)
[PROOFSTEP]
rw [lt_add_iff_pos_right] at hab hcd 
[GOAL]
case intro.intro
k : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : OrderedRing k
inst✝⁴ : OrderedAddCommGroup M
inst✝³ : Module k M
inst✝² : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝¹ : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a : k
c : M
b : k
hab : 0 < b
d : M
hcd : 0 < d
⊢ a • c + (a + b) • c + a • d < a • c + (a + b) • c + (a • d + b • d)
[PROOFSTEP]
exact add_lt_add_left (lt_add_of_pos_right _ <| smul_pos hab hcd) _
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : OrderedRing k
inst✝⁴ : OrderedAddCommGroup M
inst✝³ : Module k M
inst✝² : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝¹ : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a b : k
c d : M
hba : b < a
hdc : d < c
⊢ a • d + b • c < a • c + b • d
[PROOFSTEP]
rw [add_comm (a • d), add_comm (a • c)]
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : OrderedRing k
inst✝⁴ : OrderedAddCommGroup M
inst✝³ : Module k M
inst✝² : OrderedSMul k M
a✝ b✝ : M
c✝ : k
inst✝¹ : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a b : k
c d : M
hba : b < a
hdc : d < c
⊢ b • c + a • d < b • d + a • c
[PROOFSTEP]
exact smul_add_smul_lt_smul_add_smul hba hdc
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
hc : c < 0
⊢ c • a ≤ c • b ↔ b ≤ a
[PROOFSTEP]
rw [← neg_neg c, neg_smul, neg_smul (-c), neg_le_neg_iff]
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
hc : c < 0
⊢ -c • b ≤ -c • a ↔ b ≤ a
[PROOFSTEP]
exact smul_le_smul_iff_of_pos (neg_pos_of_neg hc)
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
h : c < 0
⊢ c⁻¹ • a ≤ b ↔ c • b ≤ a
[PROOFSTEP]
rw [← smul_le_smul_iff_of_neg h, smul_inv_smul₀ h.ne]
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
h : c < 0
⊢ c⁻¹ • a < b ↔ c • b < a
[PROOFSTEP]
rw [← smul_lt_smul_iff_of_neg h, smul_inv_smul₀ h.ne]
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
h : c < 0
⊢ a ≤ c⁻¹ • b ↔ b ≤ c • a
[PROOFSTEP]
rw [← smul_le_smul_iff_of_neg h, smul_inv_smul₀ h.ne]
[GOAL]
k : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup M
inst✝¹ : Module k M
inst✝ : OrderedSMul k M
a b : M
c : k
h : c < 0
⊢ a < c⁻¹ • b ↔ b < c • a
[PROOFSTEP]
rw [← smul_lt_smul_iff_of_neg h, smul_inv_smul₀ h.ne]
