case inl
F : Type ?u.55586
α : Type u_1
β : Type ?u.55592
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a✝ : α
n : ℕ
a : α
ha : a ≤ 0
⊢ ⌊a⌋₊ ≤ ⌈a⌉₊

case inr
F : Type ?u.55586
α : Type u_1
β : Type ?u.55592
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a✝ : α
n : ℕ
a : α
ha : 0 ≤ a
⊢ ⌊a⌋₊ ≤ ⌈a⌉₊
F : Type ?u.55586
α : Type u_1
β : Type ?u.55592
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a✝ : α
n : ℕ
a : α
⊢ ⌊a⌋₊ ≤ ⌈a⌉₊
obtain ha | ha := le_total a 0
case inl
F : Type ?u.55586
α : Type u_1
β : Type ?u.55592
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a✝ : α
n : ℕ
a : α
ha : a ≤ 0
⊢ 0 ≤ ⌈a⌉₊
case inl
F : Type ?u.55586
α : Type u_1
β : Type ?u.55592
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a✝ : α
n : ℕ
a : α
ha : a ≤ 0
⊢ ⌊a⌋₊ ≤ ⌈a⌉₊
rw [floor_of_nonpos ha]
no goals
case inl
F : Type ?u.55586
α : Type u_1
β : Type ?u.55592
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a✝ : α
n : ℕ
a : α
ha : a ≤ 0
⊢ 0 ≤ ⌈a⌉₊
exact Nat.zero_le _
no goals
case inr
F : Type ?u.55586
α : Type u_1
β : Type ?u.55592
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a✝ : α
n : ℕ
a : α
ha : 0 ≤ a
⊢ ⌊a⌋₊ ≤ ⌈a⌉₊
exact cast_le.1 ((floor_le ha).trans <| le_ceil _)