F : Type ?u.25146
α : Type u_1
β : Type ?u.25152
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a✝ : α
n✝ n a : ℕ
⊢ 0 ≤ ↑n
F : Type ?u.25146
α : Type u_1
β : Type ?u.25152
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a✝ : α
n✝ n a : ℕ
⊢ a ≤ ⌊↑n⌋₊ ↔ a ≤ n
rw [le_floor_iff, Nat.cast_le]
no goals
F : Type ?u.25146
α : Type u_1
β : Type ?u.25152
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a✝ : α
n✝ n a : ℕ
⊢ 0 ≤ ↑n
exact n.cast_nonneg