α : Type u_1
inst✝² : StrictOrderedSemiring α
inst✝¹ : Archimedean α
x : α
inst✝ : Nontrivial α
⊢ ∃ n, x ≤ ↑n
α : Type u_1
inst✝¹ : StrictOrderedSemiring α
inst✝ : Archimedean α
x : α
⊢ ∃ n, x ≤ ↑n
nontriviality α
no goals
α : Type u_1
inst✝² : StrictOrderedSemiring α
inst✝¹ : Archimedean α
x : α
inst✝ : Nontrivial α
⊢ ∃ n, x ≤ ↑n
exact (exists_nat_gt x).imp fun n => le_of_lt