α : Type u
β : Type ?u.59742
inst✝¹ : StrictOrderedSemiring α
a b c d : α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
h1 : a < c
h2 : b < d
h3 : 0 ≤ a
h4 : 0 ≤ b
b0 : 0 = b
⊢ 0 < c * d
α : Type u
β : Type ?u.59742
inst✝¹ : StrictOrderedSemiring α
a b c d : α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
h1 : a < c
h2 : b < d
h3 : 0 ≤ a
h4 : 0 ≤ b
b0 : 0 = b
⊢ a * b < c * d
rw [← b0, mul_zero]
no goals
α : Type u
β : Type ?u.59742
inst✝¹ : StrictOrderedSemiring α
a b c d : α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
h1 : a < c
h2 : b < d
h3 : 0 ≤ a
h4 : 0 ≤ b
b0 : 0 = b
⊢ 0 < c * d
exact mul_pos (h3.trans_lt h1) (h4.trans_lt h2)