case inl
F : Type ?u.27586
α : Type u_1
β : Type ?u.27592
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a✝ : α
n : ℕ
a b : α
h : a ≤ b
ha : a ≤ 0
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊

case inr
F : Type ?u.27586
α : Type u_1
β : Type ?u.27592
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a✝ : α
n : ℕ
a b : α
h : a ≤ b
ha : 0 ≤ a
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊
F : Type ?u.27586
α : Type u_1
β : Type ?u.27592
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a✝ : α
n : ℕ
a b : α
h : a ≤ b
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊
obtain ha | ha := le_total a 0
case inl
F : Type ?u.27586
α : Type u_1
β : Type ?u.27592
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a✝ : α
n : ℕ
a b : α
h : a ≤ b
ha : a ≤ 0
⊢ 0 ≤ ⌊b⌋₊
case inl
F : Type ?u.27586
α : Type u_1
β : Type ?u.27592
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a✝ : α
n : ℕ
a b : α
h : a ≤ b
ha : a ≤ 0
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊
rw [floor_of_nonpos ha]
no goals
case inl
F : Type ?u.27586
α : Type u_1
β : Type ?u.27592
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a✝ : α
n : ℕ
a b : α
h : a ≤ b
ha : a ≤ 0
⊢ 0 ≤ ⌊b⌋₊
exact Nat.zero_le _
no goals
case inr
F : Type ?u.27586
α : Type u_1
β : Type ?u.27592
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a✝ : α
n : ℕ
a b : α
h : a ≤ b
ha : 0 ≤ a
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊
exact le_floor ((floor_le ha).trans h)