α : Type u
β : Type ?u.13770
inst✝¹ : StrictOrderedSemiring α
a b c d : α
inst✝ : ExistsAddOfLE α
hba : b < a
hdc : d < c
⊢ b • c + a • d < b • d + a • c
α : Type u
β : Type ?u.13770
inst✝¹ : StrictOrderedSemiring α
a b c d : α
inst✝ : ExistsAddOfLE α
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
α : Type u
β : Type ?u.13770
inst✝¹ : StrictOrderedSemiring α
a b c d : α
inst✝ : ExistsAddOfLE α
hba : b < a
hdc : d < c
⊢ b • c + a • d < b • d + a • c
exact mul_add_mul_lt_mul_add_mul hba hdc