case inl
F : Type ?u.28566
α : Type u_1
β : Type ?u.28572
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n : ℕ
hn : n ≠ 0
ha : a ≤ 0
⊢ n ≤ ⌊a⌋₊ ↔ ↑n ≤ a

case inr
F : Type ?u.28566
α : Type u_1
β : Type ?u.28572
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n : ℕ
hn : n ≠ 0
ha : 0 ≤ a
⊢ n ≤ ⌊a⌋₊ ↔ ↑n ≤ a
F : Type ?u.28566
α : Type u_1
β : Type ?u.28572
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n : ℕ
hn : n ≠ 0
⊢ n ≤ ⌊a⌋₊ ↔ ↑n ≤ a
obtain ha | ha := le_total a 0
case inl
F : Type ?u.28566
α : Type u_1
β : Type ?u.28572
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n : ℕ
hn : n ≠ 0
ha : a ≤ 0
⊢ n ≤ 0 ↔ ↑n ≤ a
case inl
F : Type ?u.28566
α : Type u_1
β : Type ?u.28572
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n : ℕ
hn : n ≠ 0
ha : a ≤ 0
⊢ n ≤ ⌊a⌋₊ ↔ ↑n ≤ a
rw [floor_of_nonpos ha]
no goals
case inl
F : Type ?u.28566
α : Type u_1
β : Type ?u.28572
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n : ℕ
hn : n ≠ 0
ha : a ≤ 0
⊢ n ≤ 0 ↔ ↑n ≤ a
exact
  iff_of_false (Nat.pos_of_ne_zero hn).not_le
    (not_le_of_lt <| ha.trans_lt <| cast_pos.2 <| Nat.pos_of_ne_zero hn)
no goals
case inr
F : Type ?u.28566
α : Type u_1
β : Type ?u.28572
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n : ℕ
hn : n ≠ 0
ha : 0 ≤ a
⊢ n ≤ ⌊a⌋₊ ↔ ↑n ≤ a
exact le_floor_iff ha