b n : ℕ
⊢ (∀ (h : b ≤ n ∧ 1 < b),
      (let_fun this := (_ : n / b < n);
        log b (n / b) + 1) =
        0) ↔
    n < b ∨ b ≤ 1
b n : ℕ
⊢ log b n = 0 ↔ n < b ∨ b ≤ 1
rw [log, dite_eq_right_iff]
no goals
b n : ℕ
⊢ (∀ (h : b ≤ n ∧ 1 < b),
      (let_fun this := (_ : n / b < n);
        log b (n / b) + 1) =
        0) ↔
    n < b ∨ b ≤ 1
simp only [Nat.succ_ne_zero, imp_false, not_and_or, not_le, not_lt]