α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hab : a ≤ b
hb : b ≠ 0
hcd : c < d
hd : d ≠ 0
ha : a = 0
⊢ b * d ≠ 0
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hab : a ≤ b
hb : b ≠ 0
hcd : c < d
hd : d ≠ 0
ha : a = 0
⊢ a * c < b * d
rw [ha, zero_mul, zero_lt_iff]
no goals
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hab : a ≤ b
hb : b ≠ 0
hcd : c < d
hd : d ≠ 0
ha : a = 0
⊢ b * d ≠ 0
exact mul_ne_zero hb hd
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hab : a ≤ b
hb : b ≠ 0
hcd : c < d
hd : d ≠ 0
ha : ¬a = 0
hc : c = 0
⊢ b * d ≠ 0
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hab : a ≤ b
hb : b ≠ 0
hcd : c < d
hd : d ≠ 0
ha : ¬a = 0
hc : c = 0
⊢ a * c < b * d
rw [hc, mul_zero, zero_lt_iff]
no goals
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hab : a ≤ b
hb : b ≠ 0
hcd : c < d
hd : d ≠ 0
ha : ¬a = 0
hc : c = 0
⊢ b * d ≠ 0
exact mul_ne_zero hb hd