b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ n + b ≤ n * b
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ (n + b - 1) / b < n
rw [div_lt_iff_lt_mul (zero_lt_one.trans hb), ← succ_le_iff, ← pred_eq_sub_one,
  succ_pred_eq_of_pos (add_pos (zero_lt_one.trans hn) (zero_lt_one.trans hb))]
no goals
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ n + b ≤ n * b
exact add_le_mul hn hb