F : Type ?u.36275
α : Type u_1
β : Type ?u.36281
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n : ℕ
⊢ ⌊a⌋₊ < 1 ↔ a < ↑1
F : Type ?u.36275
α : Type u_1
β : Type ?u.36281
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n : ℕ
⊢ ⌊a⌋₊ = 0 ↔ a < 1
rw [← lt_one_iff, ← @cast_one α]
no goals
F : Type ?u.36275
α : Type u_1
β : Type ?u.36281
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n : ℕ
⊢ ⌊a⌋₊ < 1 ↔ a < ↑1
exact floor_lt' Nat.one_ne_zero