no goals
ι : Type ?u.88530
α : Type u_1
β : Type ?u.88536
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h1 : 0 < a
h2 : a ≤ 1
⊢ 1 ≤ 1 / a
rwa [le_one_div (@zero_lt_one α _ _ _ _ _) h1, one_div_one]