R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
⊢ clog b r = 0
rw [clog, if_neg (hr.trans_lt zero_lt_one).not_le, neg_eq_zero, Int.coe_nat_eq_zero,
  Nat.log_eq_zero_iff]
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
hb : b ≤ 1
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1

case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
hb : 1 < b
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1
cases' le_or_lt b 1 with hb hb
no goals
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
hb : b ≤ 1
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1
exact Or.inr hb
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
hb : 1 < b
⊢ ⌊r⁻¹⌋₊ ≤ 1
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
hb : 1 < b
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1
refine' Or.inl (lt_of_le_of_lt _ hb)
no goals
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
hb : 1 < b
⊢ ⌊r⁻¹⌋₊ ≤ 1
exact Nat.floor_le_one_of_le_one ((inv_nonpos.2 hr).trans zero_le_one)