α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
ha : a ≠ 0
⊢ b * a ≤ c * a ↔ b ≤ c
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
ha : a ≠ 0
⊢ a * b ≤ a * c ↔ b ≤ c
simp only [mul_comm a]
no goals
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
ha : a ≠ 0
⊢ b * a ≤ c * a ↔ b ≤ c
exact mul_le_mul_right₀ ha