case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ (n + b - 1) / b ≤ 1
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ clog b n = 1
rw [clog_of_two_le (hn.trans h) hn, clog_of_right_le_one]
case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
n_pos : 0 < n
⊢ (n + b - 1) / b ≤ 1
case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ (n + b - 1) / b ≤ 1
have n_pos : 0 < n := (zero_lt_two' ℕ).trans_le hn
case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
n_pos : 0 < n
⊢ n + b ≤ b + b
case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
n_pos : 0 < n
⊢ (n + b - 1) / b ≤ 1
rw [← lt_succ_iff, Nat.div_lt_iff_lt_mul (n_pos.trans_le h), ← succ_le_iff, ← pred_eq_sub_one,
  succ_pred_eq_of_pos (add_pos n_pos (n_pos.trans_le h)), succ_mul, one_mul]
no goals
case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
n_pos : 0 < n
⊢ n + b ≤ b + b
exact add_le_add_right h _