no goals
α : Type u
β : Type ?u.218570
inst✝ : LinearOrderedCommRing α
a b✝ c✝ d b c : α
ha : 0 ≤ a
hd : 0 ≤ d
ba : b * a ≤ max d b * max c a
cd : c * d ≤ max a c * max b d
⊢ a * b ≤ max a c * max d b
simpa [mul_comm, max_comm] using ba
no goals
α : Type u
β : Type ?u.218570
inst✝ : LinearOrderedCommRing α
a b✝ c✝ d b c : α
ha : 0 ≤ a
hd : 0 ≤ d
ba : b * a ≤ max d b * max c a
cd : c * d ≤ max a c * max b d
⊢ d * c ≤ max a c * max d b
simpa [mul_comm, max_comm] using cd