no goals
ι : Type ?u.46241
α : Type u_1
β : Type ?u.46247
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
hb : 0 < b
⊢ a⁻¹ ≤ b⁻¹ ↔ b ≤ a
rw [← one_div, div_le_iff ha, ← div_eq_inv_mul, le_div_iff hb, one_mul]