α : Type u_1
a b c✝ d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
c : α
hc : c ≠ 0
h : b * c ≤ a * c
⊢ b ≤ a
α : Type u_1
a b c✝ d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
c : α
h : a < b
hc : c ≠ 0
⊢ a * c < b * c
contrapose! h
no goals
α : Type u_1
a b c✝ d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
c : α
hc : c ≠ 0
h : b * c ≤ a * c
⊢ b ≤ a
exact le_of_le_mul_right hc h