no goals
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
⊢ a / b ≤ 1 ↔ a ≤ b
rw [← mul_le_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]