F : Type ?u.124074
α : Type u_1
β : Type ?u.124080
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
ha : a ≤ 0
⊢ ↑⌊a⌋ ≤ 0
F : Type ?u.124074
α : Type u_1
β : Type ?u.124080
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
ha : a ≤ 0
⊢ ⌊a⌋ ≤ 0
rw [← @cast_le α, Int.cast_zero]
no goals
F : Type ?u.124074
α : Type u_1
β : Type ?u.124080
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
ha : a ≤ 0
⊢ ↑⌊a⌋ ≤ 0
exact (floor_le a).trans ha