case pos
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hab : a ≤ b * c
h : c = 0
⊢ a * c⁻¹ ≤ b

case neg
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hab : a ≤ b * c
h : ¬c = 0
⊢ a * c⁻¹ ≤ b
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hab : a ≤ b * c
⊢ a * c⁻¹ ≤ b
by_cases h : c = 0
no goals
case pos
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hab : a ≤ b * c
h : c = 0
⊢ a * c⁻¹ ≤ b
simp [h]
no goals
case neg
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hab : a ≤ b * c
h : ¬c = 0
⊢ a * c⁻¹ ≤ b
exact le_of_le_mul_right h (by simpa [h] using hab)
no goals
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hab : a ≤ b * c
h : ¬c = 0
⊢ a * c⁻¹ * c ≤ b * c
simpa [h] using hab