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