case zero
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
⊢ clog b ↑Nat.zero = ↑(Nat.clog b Nat.zero)

case succ
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b n : ℕ
⊢ clog b ↑(Nat.succ n) = ↑(Nat.clog b (Nat.succ n))
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b n : ℕ
⊢ clog b ↑n = ↑(Nat.clog b n)
cases' n with n
no goals
case zero
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
⊢ clog b ↑Nat.zero = ↑(Nat.clog b Nat.zero)
simp [clog_of_right_le_one]
no goals
case succ
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b n : ℕ
⊢ clog b ↑(Nat.succ n) = ↑(Nat.clog b (Nat.succ n))
rw [clog_of_one_le_right, (Nat.ceil_eq_iff (Nat.succ_ne_zero n)).mpr] <;> simp