k : Type u_2
M : Type u_1
N : Type ?u.81455
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
k : Type u_2
M : Type u_1
N : Type ?u.81455
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
rw [add_comm (a • d), add_comm (a • c)]
no goals
k : Type u_2
M : Type u_1
N : Type ?u.81455
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
exact smul_add_smul_lt_smul_add_smul hba hdc