no goals
α : Type u
β : Type ?u.60876
inst✝ : StrictOrderedSemiring α
a b c d : α
⊢ a < c → b < d → 0 ≤ a → 0 ≤ b → a * b < c * d
classical
exact Decidable.mul_lt_mul''
no goals
α : Type u
β : Type ?u.60876
inst✝ : StrictOrderedSemiring α
a b c d : α
⊢ a < c → b < d → 0 ≤ a → 0 ≤ b → a * b < c * d
exact Decidable.mul_lt_mul''