F : Type ?u.47671
α✝ : Type ?u.47674
β : Type ?u.47677
inst✝³ : LinearOrderedSemiring α✝
inst✝² : FloorSemiring α✝
a✝ : α✝
n : ℕ
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : FloorSemiring α
z : ℤ
a : ℕ
⊢ ↑z ≤ ↑a ↔ z ≤ ↑a
F : Type ?u.47671
α✝ : Type ?u.47674
β : Type ?u.47677
inst✝³ : LinearOrderedSemiring α✝
inst✝² : FloorSemiring α✝
a✝ : α✝
n : ℕ
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : FloorSemiring α
z : ℤ
a : ℕ
⊢ ⌈↑z⌉₊ ≤ a ↔ Int.toNat z ≤ a
simp
no goals
F : Type ?u.47671
α✝ : Type ?u.47674
β : Type ?u.47677
inst✝³ : LinearOrderedSemiring α✝
inst✝² : FloorSemiring α✝
a✝ : α✝
n : ℕ
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : FloorSemiring α
z : ℤ
a : ℕ
⊢ ↑z ≤ ↑a ↔ z ≤ ↑a
norm_cast