no goals
α : Type u_1
a✝ b✝ c✝ d✝ x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
a b c d : α
hb : b ≠ 0
hd : d ≠ 0
⊢ a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b
rw [mul_inv_le_iff₀ hb, mul_right_comm, le_mul_inv_iff₀ hd]