no goals
α : Type u
inst✝² : CommGroup α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
⊢ a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b
rw [mul_comm c, mul_inv_le_inv_mul_iff, mul_comm]