F : Type ?u.26833
α : Type u_1
β : Type ?u.26839
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
n : ℕ
ha : 0 ≤ 0
⊢ ⌊0⌋₊ = 0
F : Type ?u.26833
α : Type u_1
β : Type ?u.26839
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : a ≤ 0
⊢ a = 0 → ⌊a⌋₊ = 0
rintro rfl
no goals
F : Type ?u.26833
α : Type u_1
β : Type ?u.26839
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
n : ℕ
ha : 0 ≤ 0
⊢ ⌊0⌋₊ = 0
exact floor_zero